Properties of Canonical Forms

Created on March 5, 2013, 10:49 p.m. by Hevok & updated by Hevok on May 2, 2013, 5:31 p.m.

The Canonical Forms are produces by the applications of Equivalences, with one exception which is the Skolum Normal Form.

If F is a Formula and G is the Prenex Normal Form, between them are only Equivalence Transformations. Therefore both are equivalent, i.e. whenever F is True than also G is True. The same holds for the Relation between the Skolem Normal Form (H), the Clausal Form (K), because in this Transformation one also only applies equivalence Transformations. Therefore H and K are both equivalent, which means whenever H is True than K is also True.

The only difference is between the Prenex Normal Form and the Skolem Normal Form as they are not equivalent, because there one made Substations. The Existential Quantifiers are replaced by a Constants or a Function. Thus, it does not hold whenever F is True that K is also True. So they are not equivalent. But as they are closely related with each other, there is another Connection which goes vice versa. It holds that if F, the original Formula is not satisfiable, which means if F is a Contradiction, then also K, although it is not really equivalent to F, must also be a Contradiction. So the Contradiction is maintained through this Transformations. This is the Basic and the Foundation of Resolution.

  • Let F be a Formula,
  • G is the Prenex Normal From of F,
  • H is the Skolem Normal Form of G,
  • K is the Clausal Form of H.
  • Then F ≡ G and H ≡ K but usually F ≢ K.
  • Nevertheless it holds, that
  • F is not Satisfiable (a Contraction), if K is a Contradiction. (Foundation of the Resolution)

Tags: equivalence, transformation, equality, equal, foundation, logic
Parent: Canonical Form

Update entry (Admin) | See changes

Comment on This Data Unit