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))