logic-classes-1.4.8: Framework for propositional and first order logic, theorem proving

Data.Logic.Normal.Clause

Description

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

Synopsis

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

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