Safe Haskell | None |
---|

# Documentation

The `toNNF`

function converts expressions to negation normal form. This
function is total: it's defined for all expressions, not just those which
only use negation, conjunction and disjunction, although all expressions in
negation normal form do in fact only use those connectives.

The conversion is carried out by replacing any condtitionals or
biconditionals with equivalent expressions using only negation, conjunction
and disjunction. Then de Morgan's laws are applied to convert negated
conjunctions and disjunctions into the conjunction or disjunction of the
negation of their conjuncts: `¬(φ ∧ ψ)`

is converted to `(¬φ ∨ ¬ψ)`

while `¬(φ ∨ ψ)`

becomes `(¬φ ∧ ¬ψ)`

.

The `toCNF`

function converts expressions to conjunctive normal form: a
conjunction of clauses, where a clause is a disjunction of literals
(variables and negated variables).

The conversion is carried out by first converting the expression into negation normal form, and then applying the distributive law.

Because it first applies `toNNF`

, it is a total function and can handle
expressions which include conditionals and biconditionals.

The `toDNF`

function converts expressions to disjunctive normal form: a
disjunction of clauses, where a clause is a conjunction of literals
(variables and negated variables).

The conversion is carried out by first converting the expression into negation normal form, and then applying the distributive law.

Because it first applies `toNNF`

, it is a total function and can handle
expressions which include conditionals and biconditionals.