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.

## Comment on This Data Unit