Canonical Form

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.

  • For all of the Equivalence Classes one designates a most simple and unique representative.
  • These representatives are called Canonical Forms or Normal Forms.
  • These representatives are called Canonical Forms or Normal Forms
  • simple example
  • we write ¬F instead of ¬¬¬¬¬F

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

    • b1 ∨ b2 ∨ ... bn
    • a simple clause can also written as {b1, b2. ..., bn}
  • A Conjunctive Normal Form (CNF) is a conjunction of clauses
  • A Clausal Normal Form corresponds to a Conjunctive Normal Form
    • {{b1, b2, ...,bn}, ..., {c1, c2, ..., cm}}

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.


 ( (∃Y) q(Y) ) → ( (∃X) (∀Y) p(X,Y) )
  1. Negation Normal Form: move all negations inwards

     ¬( (∃Y) q(Y) ) ∨  ( (∃X) (∀Y) p(X,Y) )
     ( (∀Y) ¬q(Y) ) ∨  ( (∃X) (∀Y) p(X,Y) )
  2. 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) )
  3. Skolum Normal Form: remove Existential Quantifiers

     [X/f(Y)](∀Y1)(∀Z) ( ¬q(Y) ) ∨  (  p(f(Y),Z) )
  4. 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)}

Tags: form, equivalence, normal, transformation
Categories: Concept
Parent: Logic
Children: Commutativity and Quantifiers, Conjunctive Normal Form, Logical Equivalences, Negation Normal Form, Prenex Normal Form, Properties of Canonical Forms, Skolem Normal Form, Unified Formula

Update entry (Admin) | See changes

Comment on This Data Unit