hatt-1.5.0.3: A truth table generator for classical propositional logic.

Data.Logic.Propositional.NormalForms

Description

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.

Synopsis

# 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.