Clause Normal Form

Clause Normal Form (CNF) is a sub-language of 1st order logic. A clause is an expression of the form L1 |... | Lm where each Li is a literal. Clauses are denoted by uppercase letters with a superscript |, e.g., C|.

There are satisfiability preserving transformations from 1st order logic to CNF, i.e., if a set of (1st order) formulae are satisfiable, then their CNF is satisfiable. Conversely, if the CNF of a set of formulae is unsatisfiable, then the formulae are unsatisfiable. This is then useful for showing logical consequence. The benefit of converting to CNF is that more is possible using just the Herbrand interpretations. Computationally, CNF is easier to work with, and is the form used by the resolution inference rule.


Transforming to Clause Normal Form

There are several algorithms for this conversion, but they all have some parts in common, and all have similarities. The best allgorithm is the one which produces the CNF which is most easily shown to be unsatisfiable. In general such a determination is impossible to make, but a common measure is to aim to produce a CNF with the fewest symbols (where a symbol is a variable, predicate, or constant). The key feature of all the algorithms is that they are satisfiability preserving.

The starting point is a set of closed formulae. As a preprocessing step, all variables must be renamed apart.

Rename variables apart

The first operation is to simplify the formulae so that they contain only the , , &, | and ~ connectives. This is done by using known logical identities. The identities are easily verified using truth tables, to show that the original formula has the same value as the simplified formula for all possible interpretations of the component formulae, denoted by uppercase variable letters P and Q.

Simplify
FormulaRewrites to
P <~> Q (P | Q) & (~P | ~Q)
P <=> Q (P => Q) & (Q => P)
P => Q ~P | Q

The second operation is to move negations in so that they apply to only atoms. This is done by using known logical identities (including De Morgan's laws), which are easily verified as above. After moving negations in the formulae are in literal normal form.

Move negations in
FormulaRewrites to
~∀X P ∃X ~P
~∃X P ∀X ~P
~(P & Q) (~P | ~Q)
~(P | Q) (~P & ~Q)
~~P P

The third operation is to move quantifiers out so that each formula is in the scope of all the quantifiers in that formula. This is done by using known logical identities, which are easily verified as above. In these identities, if the variable X already exists in Q, it is renamed to a new variable name that does not exist in the formula. After moving quantifiers out the formulae are in prenex normal form.

Move quantifiers out
FormulaRewrites to
∀X P & Q ∀X (P & Q)
∃X P & Q ∃X (P & Q)
Q & ∀X P ∀X (Q & P)
Q & ∃X P ∃X (Q & P)
∀X P | Q ∀X (P | Q)
∃X P | Q ∃X (P | Q)
Q | ∀X P ∀X (Q | P)
Q | ∃XP ∃X (Q | P)

The fourth operation is to Skolemize to remove existential quantifiers. This step replaces existentially quantified variables by Skolem functions and removes all quantifiers. The variables remaining after Skolemization are all implicitly universally quantified. Whereas the previous three operations maintain equivalence between the original and transformed formulae, Skolemization does not. However, Skolemization does maintain the satisfiability of the formulae, which is what is required for the overall goal of establishing logical consequence. After Skolemization the formulae are in Skolem normal form.

Skolemize
FormulaRewrites to
Initially Set γ = {}
∀X P P
and set γ = γ ∪ {X}
∃X P P[X/x(γ)]
where x is a new Skolem functor.

The fifth operation is to distribute disjunctions so that the formulae are conjunctions of disjunctions. This is done by using known logical identities, which are easily verified as above. After distributing disjunctions the formulae are in conjunctive normal form.

Distribute disjunctions
FormulaRewrites to
P | (Q & R) (P | Q) & (P | R)
(Q & R) | P (Q | P) & (R | P)

The last operation is to convert to Clause Normal Form. This is done by removing the conjunctions, to form a set of clauses.

Convert to CNF
FormulaRewrites to
P1 & ... & Pn {P1,...,Pn}

Example
1st order formula
∀Y (∀X (taller(Y,X) | wise(X)) => wise(Y))

Simplify
∀Y (~∀X (taller(Y,X) | wise(X)) | wise(Y))

Move negations in
∀Y (∃X (~taller(Y,X) & ~wise(X)) | wise(Y))

Move quantifiers out
∀Y (∃X ((~taller(Y,X) & ~wise(X)) | wise(Y)))

Skolemize
∃X ((~taller(Y,X) & ~wise(X)) | wise(Y)) γ = {Y}
(~taller(Y,x(Y)) & ~wise(x(Y))) | wise(Y)

Distribute disjunctions
(~taller(Y,x(Y)) | wise(Y)) & (~wise(x(Y)) | wise(Y))

Convert to CNF
{ ~taller(Y,x(Y)) | wise(Y),
~wise(x(Y)) | wise(Y) }


Special Forms

Clauses may be expressed in Kowalski form. Kowalski form forms the antecedent of an implication by conjoining the atoms of the negative literals in a clause, and forms the consequent from the disjunction of the positive literals.

Example
~taller(Y,x(Y)) | wise(Y) | ~wise(x(Y)) | taller(x(Y),Y)
is written as
taller(Y,x(Y)) & wise(x(Y)) => wise(Y) | taller(x(Y),Y)
If the antecedent is empty it is set to TRUE, and if the consequent is empty it is set to FALSE.

Horn clauses are clauses that have one or zero positive literals. Sets of Horn clauses are also called Horn.

Example
~taller(Y,x(Y)) | wise(Y) | ~wise(x(Y))
~wise(geoff) | ~taller(Person,brother_of(jim))
are Horn clauses. Written in Kowalski form, these Horn clauses are :
taller(Y,x(Y)) & wise(x(Y)) => wise(Y)
wise(geoff) & taller(Person,brother_of(jim)) => FALSE

Non-Horn clauses are clauses that have two or more positive literals. Sets of clauses that contain one or more non-Horn clauses are also called non-Horn.

Example
~taller(Y,x(Y)) | ~wise(Y) | wise(x(Y)) | taller(x(Y),x(x(Y)))
wise(X) | wise(brother_of(X))
are non-Horn clauses. Written in Kowalski form, these non-Horn clauses are :
taller(Y,x(Y)) & wise(Y) => wise(x(Y)) | taller(x(Y),x(x(Y)))
TRUE => wise(X) | wise(brother_of(X))

In terms of ATP, the disjunction of positive literals in non-Horn clauses corresponds to a choice point in any goal directed search. This is a source of search. Thus, in general, Horn problems are easier than non-Horn problems.


Exercises

Convert the following to CNF:


The Quest for Logical Consequence

To show that C is a logical consequence of A, it is necessary to:

S' is unsatisfiable iff S = CNF(S') is unsatisfiable


Exam Style Questions

  1. Convert the following to CNF. Notation: & for AND, | for OR, ! for universal quantifier, ? for existential quantifier.
     ( ? [Y] :
       ! [X] :
         ( element(X,Y)
       <=> element(X,X) )
    => ~ ( ! [X1] :
           ? [Y1] :
           ! [Z] :
             ( element(Z,Y1)
           <=> ~ e1ement(Z,X1) ) ) ) 
  2. Explain, with examples, the difference between Horn and non-Horn clauses.
  3. Explain, with examples, what is meant by Kowalski form for clauses. Why is Kowalski form important?