Crux.Expression.RewriteRule.ConsensusTheorem (crux v0.1.3)

Copy Markdown View Source

Rewrite rule that applies the consensus theorem to eliminate redundant clauses.

See: https://en.wikipedia.org/wiki/Consensus_theorem

Applies the transformations:

  • (A OR B) AND (NOT A OR C) AND (B OR C) = (A OR B) AND (NOT A OR C)
  • (A AND B) OR (NOT A AND C) OR (B AND C) = (A AND B) OR (NOT A AND C)

The consensus theorem states that in certain patterns, one clause can be derived from two others and is therefore redundant.