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

Copy Markdown View Source

Rewrite rule that applies the distributive law to convert expressions to CNF.

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

Applies the transformations:

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

This transformation pushes OR operations inside AND operations, which is necessary for achieving Conjunctive Normal Form (CNF).