Data.Logic.Normal.Clause

A series of transformations to convert first order logic formulas into (ultimately) Clause Normal Form.

 1st order formula:
   ∀Y (∀X (taller(Y,X) | wise(X)) => wise(Y))

Simplify
   ∀Y (~∀X (taller(Y,X) | wise(X)) | wise(Y))

Move negations in - Negation Normal Form
   ∀Y (∃X (~taller(Y,X) & ~wise(X)) | wise(Y))

Move quantifiers out - Prenex Normal Form
   ∀Y (∃X ((~taller(Y,X) & ~wise(X)) | wise(Y)))

Distribute disjunctions
   ∀Y ∃X ((~taller(Y,X) | wise(Y)) & (~wise(X) | wise(Y)))

Skolemize  - Skolem Normal Form
   ∀Y (~taller(Y,x(Y)) | wise(Y)) & (~wise(x(Y)) | wise(Y))

Convert to CNF
   { ~taller(Y,x(Y)) | wise(Y),
     ~wise(x(Y)) | wise(Y) } 

Documentation

clauseNormalForm :: forall formula atom term v f lit m. (Monad m, FirstOrderFormula formula atom v, PropositionalFormula formula atom, Atom atom term v, Term term v f, Literal lit atom, Ord formula, Ord lit) => formula -> SkolemT v term m (Set (Set lit))

Convert to Skolem Normal Form and then distribute the disjunctions over the conjunctions:

 Formula      Rewrites to
 P | (Q & R)  (P | Q) & (P | R)
 (Q & R) | P  (Q | P) & (R | P)

cnfTrace :: forall m formula atom term v p f lit. (Monad m, FirstOrderFormula formula atom v, PropositionalFormula formula atom, Atom atom term v, AtomEq atom p term, Term term v f, Literal lit atom, Ord formula, Ord lit) => (v -> Doc) -> (p -> Doc) -> (f -> Doc) -> formula -> SkolemT v term m (String, Set (Set lit))