Clause Normal Form

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. Computationally, CNF is easier to work with, and is the form used by the resolution inference rule.

Transforming to Clause Normal Form

The starting point is a set of closed formulae.

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
Formula	Rewrites 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
Formula	Rewrites 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
Formula	Rewrites 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
Formula	Rewrites 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
Formula	Rewrites 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
Formula	Rewrites 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

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

• ~∃X (s(X) & q(X))
  Answer: { ~s(X) | ~q(X) }
• ∀X (p(X) => (q(X) | r(X)))
  Answer: { ~p(X) | q(X) | r(X) }
• ~∃X (p(X) => ∃X q(X))
  Answer: { p(X), ~q(X) }
• ∀X (q(X) | r(X) => s(X))
  Answer: { ~q(X) | s(X), ~r(X) | s(X) }
• ∃X (p => f(X))
  Answer: { ~p | f(skX) }
• ∃X (p <=> f(X))
  Answer: { ~p | f(skX), p | ~f(skX) }
• ∀Z ∃Y ∀X (f(X,Y) <=> (f(X,Z) & ~f(X,X)))
  Answer: { ~f(A,skA(B)) | f(A,B), ~f(A,skA(B)) | ~f(A,A), ~f(A,B) | f(A,A) | f(A,skA(B)) }
• ∀X ∀Y (q(X,Y) <=> ∀Z (f(Z,X) <=> f(Z,Y)))
  Answer: { ~q(A,B) | ~ f(C,A) | f(C,B), ~ q(A,B) | ~ f(C,B) | f(C,A), f(sk1(A,B),B) | f(sk1(A,B),A) | q(B,A), f(sk1(A,B),B) | ~ f(sk1(A,B),B) | q(B,A), ~ f(sk1(A,B),A) | f(sk1(A,B),A) | q(B,A), ~ f(sk1(A,B),A) | ~ f(sk1(A,B),B) | q(B,A) }
• ∀X ∃Y ((p(X,Y) <= ∀X ∃T q(Y,X,T) ) => r(Y))
  Answer: { ~ p(A,sk1(A)) | r(sk1(A)), q(sk1(A),B,sk2(B,A)) | r(sk1(A)) }
• ∀X ∀Z (p(X,Z) => ∃Y ~ (q(X,Y) | ~r(Y,Z)))
  Answer: TBA

Satisfiability Preservation

Proof
A formula is equivalent to its simplified form Directly from the truth tables for the connectives. A simplified formula is equivalent to its literal normal form Consider, for example, the rewriting of ~∀X P to ∃X ~P : ~∀X P is TRUE in an interpretation I iff ∀X P is FALSE in I iff For some element e in the domain of I, P{X/e} is FALSE in I iff ~P{X/e} is TRUE in I iff ∃X ~P is TRUE in I. Thus ~∀X P is equivalent to ∃X ~P. Similar argument establishes the equivalence of formulae rewritten using the other literal normal form rewritings. A simplified formula is equivalent to its prenex normal form Consider, for example, the rewriting of ∀X P & Q to ∀X (P & Q) : ∀X P & Q is TRUE in an interpretation I iff ∀X P is TRUE in I and Q is TRUE in I iff for all elements e in the domain of I, P{X/e} is TRUE in I, and for all elements e in the domain of I, Q{X/e} is TRUE in I iff for all elements e in the domain of I (P & Q){X/e} is TRUE in I iff ∀X (P & Q) is TRUE in I Thus ∀X P & Q is equivalent to ∀X (P & Q). Similar argument establishes the equivalence of formulae rewritten using the other prenex normal form rewritings. A formula is satisfiable iff its Skolem normal form is satisfiable The first rewriting, which eleminates universal quantifiers, has no effect as the universal quantifiers are still there implicitly. Consider the rewriting of ∃X P to P[X/x(γ)] Let γ be of the form X1,...,Xn, i.e., X1,...,Xn are the (implicitly) universally quantified variables at this point. If ∃X P is satisfiable with model I, then for all substitutions θ = {X1/e1,...,Xn/en}, there exists a domain element e such that Pθ{X/e} is TRUE in I. Extend I to include the function mappings x(e1,...,en) => e, for each θ. Then Pθ[X/x(γ)] is TRUE in the extended interpretation. As this is the case for all substitutions θ, I is a model for P[X/x(γ)], which is thus satisfiable. If P[X/x(γ)] is satisfiable with model I, then for all substitutions θ = {X1/e1,...,Xn/en}, where each ei is from the domain of I, P[X/x(γ)]θ is TRUE in I. Let e be the interpretation of x(γ)θ in I. Then Pθ{X/e} is TRUE in I. As this is the case for all substitutions θ, I is a model for ∃X P which is thus satisfiable. A formula is equivalent to its conjunctive normal form This is evident from the definitions of the connectives being manipulated. A formula is satisfiable iff its clause normal form is satisfiable This is evident from the definitions of & and satisfiability of sets. The above points combined prove the theorem.
Example
Translating the formula ∀Y (∀X ~taller(X,Y) => wise(Y)) ∀Y (∀X ~taller(X,Y) => wise(Y)) is equivalent to its simplified form ∀Y (~∀X ~taller(X) | wise(Y)). Directly from the truth tables for the connectives. ∀Y (~∀X ~taller(X,Y) | wise(Y)) is equivalent to its literal normal form ∀Y (∃X taller(X,Y) | wise(Y)) For Y = ... ~∀X ~taller(X,) is TRUE in I = D = { , } F = { geoff → , jim → , brother_of() → , brother_of() → } R = { wise() → FALSE, wise() → TRUE, taller(,) → FALSE, taller(,) → FALSE, taller(,) → TRUE, taller(,) → FALSE } iff ∀X ~taller(X,) is FALSE in I iff ~taller(,) is FALSE in I, or ~taller(,) is FALSE in I iff ~~taller(,) is TRUE in I, or ~~taller(,) is TRUE in I iff ∃X ~~taller(X,) is TRUE in I. And similarly for Y = . ∀Y (∃X taller(X,Y) | wise(Y)) is equivalent to its prenex normal form ∀Y ∃X (taller(X,Y) | wise(Y)) ∀Y (∃X taller(X,Y) | wise(Y)) is TRUE in I (as above) iff ∃X taller(X,) | wise() is TRUE in I and ∃X taller(X,) | wise() is TRUE in I iff taller(,) | wise() is TRUE in I and taller(,) | wise() is TRUE in I iff ∀Y (taller(,Y) | wise(Y) is TRUE in I iff ∀Y ∃X (taller(X,Y) | wise(Y)) is TRUE in I ∀Y ∃X (taller(X,Y) | wise(Y)) satisfiable iff its Skolem normal form taller(x(Y),Y) | wise(Y) is satisfiable After dropping the ∀Y, γ = [Y] If ∃X (taller(X,Y) | wise(Y)) is satisfiable, then for the substitution θ = {Y/} there exists the domain element such that taller(,) | wise() is TRUE in I. Extend I to include the function mapping x() => . Then taller(x(),) | wise() is TRUE in the extended interpretation. Similarly, for the substitution θ = {Y/}, extend I to include the function mapping x() => . Therefore the extended I can be extended a model for taller(x(Y),Y) | wise(Y), which is thus satisfiable. If taller(x(Y),Y) | wise(Y) is satisfiable with model I = D = { , } F = { geoff → , jim → , brother_of() → , brother_of() → , x() → , x() → } R = { wise() → FALSE, wise() → TRUE, taller(,) → FALSE, taller(,) → FALSE, taller(,) → TRUE, taller(,) → FALSE } then for the substitution θ = {Y/}, taller(x(),) | wise() is TRUE in I. is the interpretation of x() in I. Then taller(,) | wise() is TRUE in I. As this is the case for all substitutions θ, I can be extended a model for ∃X (taller(X,Y) | wise(Y)), which is thus satisfiable.

The Quest for Logical Consequence

• Show that S' = Ax U {~C} is unsatisfiable.

• Show that 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?
4. Prove that a set of formulae is satisfiable iff its clause normal form is satisfiable.