Data.Logic.Propositional.NormalForms

The functions exposed by this module convert expressions of type Expr into different normal forms: negation normal form via toNNF, conjunctive normal form via toCNF and disjunctive normal form via toDNF. All these functions are total.

Documentation

toNNF :: Expr -> Expr

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 (¬φ ∧ ¬ψ).

toCNF :: Expr -> Expr

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.

toDNF :: Expr -> Expr

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.