Created on March 5, 2013, 9:22 p.m. by Hevok & updated by Hevok on May 2, 2013, 5:31 p.m.
Canonical Forms are needed because for every Formula there exist infinity many logically Equivalent Formulas.
For all of Equivalence Classes it is difficult to find a true equivalence as the same Knowledge/Formula with the same truth Values can be expressed in various different ways. Therefore one need a unique standard way to express a given boolean Formula. This Standard Form, the Normal Form is the Canonical Form.
If one finds a unique Representator for an unique representation of the equivalent class for all Formulas that represent the same notation or same Knowledge, then one ends up in the Canonical Form which makes it rather simple to compare two given Formulas.
If two formulas are transformed in the canonical form one can do a simple syntactical match to see whether they compute the same values.
The Canonical form can be represented as Conjunctive Normal Form or the Clausal Form. Conjunctive Normal Form is Conjunction of Disjunctions which can also be represented as a Clausal Form.
A Clause
itself is nothing else than a finite Disjunction of Literals. A Literal might be a positive or negative Variable for example.
A clause can be written in curly braces with single Literals where the commas are interpreted as Disjunctions.
Goal: Transformation of formulas into Clausal Form.
(a∧(b∨¬c)∧(a∨d)) -> {a,{b,¬c},{a,d}}
(Conjunctive Normal Form) (Clausal Form)
A Clause is a fine disjunctive of literals
A arbitrary Formula can be transformed into a canonical Form or a Clausal Form.
For First Order Logic one needs four different Steps. Each single step defines a special Normal Form, where the last Form is the Conjunctive Normal Form, i.e. Clausal Form.
The first one is the Negation Normal Form where one tries to move all Negations inwards the Formula. In the Prenex Normal Form on tries to move all Quantifiers in front of the Formulas. In the Skolem Normal Form one tries to remove all essential Quantifiers. Then when one has only Universal Quantifiers, one does not need to write them and transforms it into a Conjunctive Normal Form/Clausal Form.
Example:
( (∃Y) q(Y) ) → ( (∃X) (∀Y) p(X,Y) )
Negation Normal Form: move all negations inwards
¬( (∃Y) q(Y) ) ∨ ( (∃X) (∀Y) p(X,Y) )
( (∀Y) ¬q(Y) ) ∨ ( (∃X) (∀Y) p(X,Y) )
Prenex Normal Form: bind Qantifiers to different Variables and put all Quantifiers in front
[Y/Z]: ( (∀Y) ¬q(Y) ) ∨ ( (∃X) (∀Z) p(X,Z) )
(∀Y)(∃X)(∀Z) ( ¬q(Y1) ) ∨ ( p(X,Z) )
Skolum Normal Form: remove Existential Quantifiers
[X/f(Y)](∀Y1)(∀Z) ( ¬q(Y) ) ∨ ( p(f(Y),Z) )
Conjuctive Normal Form (Clausal Form): remove Universal Quantifiers, transform into a Conjunction of Disjunctions:
¬q(Y) ) ∨ p(f(Y),Z)
{¬q(Y), p(f(Y),Z)}
Comment on This Data Unit