Transforming to Clause Normal Form

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
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/sk_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 - Propositional
Axioms = { p | ~(~q & ~r) r => (p | q) (q & r) => p ~p | q | r } Conjecture = q | r

Example - 1st order

∀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,sk_X(Y)) & ~wise(sk_X(Y))) | wise(Y) Distribute disjunctions (~taller(Y,sk_X(Y)) | wise(Y)) & (~wise(sk_X(Y)) | wise(Y)) Convert to CNF { ~taller(Y,sk_X(Y)) | wise(Y), ~wise(sk_X(Y)) | wise(Y) }

Special Forms

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(X1) }
• ∀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
• In TPTP syntax fof(a,axiom,! [X,Z] : (p(X,Z) => ~ ! [Y] : (q(X,Y) | ~r(Y,Z)))).

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 Q is TRUE in I (Q does not contain X) 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/sk_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 domain substitutions θ = {X1/e1,...,Xn/en}, there exists a domain element e such that Pθ{X/e} is TRUE in I. Extend I to I', to include the function mappings sk_X(e1,...,en) => e, for each θ. Then Pθ[X/sk_X(γ)] is TRUE in the extended interpretation. As this is the case for all substitutions θ, I' is a model for P[X/sk_X(γ)], which is thus satisfiable. If P[X/sk_X(γ)] is satisfiable with model I, then for all domain substitutions θ = {X1/e1,...,Xn/en}, where each ei is from the domain of I, P[X/sk_X(γ)]θ is TRUE in I. Let e be the interpretation of sk_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(sk_X(Y),Y) | wise(Y) is satisfiable After dropping the ∀Y, γ = [Y] If ∃X (taller(X,Y) | wise(Y)) is satisfiable with model I = D = { , } F = { geoff → , jim → , brother_of() → , brother_of() → } R = { wise() → FALSE, wise() → TRUE, taller(,) → FALSE, taller(,) → FALSE, taller(,) → TRUE, taller(,) → FALSE } then For the substitution θ = {Y/} there exists the domain element such that taller(,) | wise() is TRUE in I. Extend I to I' to include the function mapping sk_X() => . Then taller(sk_X(),) | wise() is TRUE in the extended interpretation. For the substitution θ = {Y/}, there exists the domain element such that taller(,) | wise() is TRUE in I. Extend I to I', to include the function mapping sk_X() => . Then taller(sk_X(),) | wise() is TRUE in the extended interpretation. Therefore I' is a model for taller(sk_X(Y),Y) | wise(Y), which is thus satisfiable. If taller(sk_X(Y),Y) | wise(Y) is satisfiable with model I = D = { , } F = { geoff → , jim → , brother_of() → , brother_of() → , sk_X() → , sk_X() → } R = { wise() → FALSE, wise() → TRUE, taller(,) → FALSE, taller(,) → FALSE, taller(,) → TRUE, taller(,) → FALSE } then For the substitution θ = {Y/}, taller(sk_X(),) | wise() is TRUE in I. is the interpretation of sk_X() in I. Then taller(,) | wise() is TRUE in I. For the substitution θ = {Y/}, taller(sk_X(),) | wise() is TRUE in I. is the interpretation of sk_X() in I. Then taller(,) | wise() is TRUE in I. I is thus a model for ∃X (taller(X,Y) | wise(Y)), which is thus satisfiable.

The Quest for Logical Consequence

• Show that every model of Ax is a model of C
  OR
• Show that Ax ∪ {~C} is unsatisfiable.

• Show that CNF(Ax ∪ {~C}) 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.