Converting Arbitrary wffs to Conjunctions of Clauses

Converting Arbitrary wffs to Conjunctions of Clauses

It is a procedure, which gains efficiency from the fact that it operates on those statements that have been converted to a very convenient standard form it proofs by refutation. For example contradiction. 

Roman who know Marcus either hated Caeser or thought anyone who hates anyone is crazy. We could represent that in the wff. 

        ∀X: [Roman (x) ∧ know (x, Marcus)] [hate (x, Caeser) V (∀y : ヨz : hate (y, z) → thinkcrazy (x, y))] 

Conjunctive Normal Form 

Algorithm: Convert into clause form 

1) Eliminate → using the fact that a → b is equivalent to ㄱa V b. 

        ∀x : [Roman (x) ∧ know (x, Marcus)] V [hate (x, Caesar) V (∀y : ㄱヨz: hate (y, .z) V thinkcrazy (x, y)))] 

2) Reduce the scope of each ㄱ to a single term using fact 

        ㄱ(ㄱP) = P 

Demorgan's law 

        [ㄱ(a ∧ b)= ㄱa ⋁ㄱb and ㄱ(a ⋁ b) = ㄱa ∧ ㄱb]

        [∀x: P(x) = ヨx : ㄱP(x) ㄱEx: P(x) = ∀x : ㄱP(x)]

        Thus [ㄱRoman(x) ⋁ㄱknown(x, Marcus)] 

        (hate (x, Caesar) ⋁ (∀y : ∀z ㄱhate(y, z) ⋁ thinkcrazy(x, y))] 

3) Standardize variable so that each quantifier binds a unique variable. Since variables are just dummy names, this process cannot effect the truth value of wff. 

        ∀x : P(x) ⋁ ∀x : Q(x) 

        ∀x : P(x) ⋁ ∀y : Q(Y) 

4) Move all the quantifiers to the left of the formula without changing their relative order. This is possible as there is no conflict among variable names. 

        ∀x : ∀y = ∀z : [ ㄱRoman (x) v know (x, Marcus)] v [hate (x, Caesar) v (ㄱhate (y; z) v thinkcrazy (x, y))] 

This point formula is called pernex form. It consists of prefix of quantifiers. 

5) Eliminate existing entail quantifiers by substituting for the valuable a reference to a function. Function must be defined for each replacement.

        ∃y : President (Y₁) 

        President (S₁) 

S₁ produces value that satisfies president.

If existential quantifiers occurs within the scope of universal quantifiers. 

        ∀x : ∃y : father of (y, x) y depends as x 

        ⇒ ∀x : Father of, (S₂ (x), X) 

These functions are called skolem functions. 

argument ⟶ skolem constant. 

6) Drop the prefix, at this point all remaining variables are universally quantified. 

Thus [ㄱRoman (x) v ㄱknow (x, Marcus)] v [hate (x, Caesar) v (ㄱhate (y, z) v thinkcrazy (x, y))]

7) Convert the matrix into a conjunction of disjuncts or (a Ʌ b) V c = (a V c) Ʌ (b V c) a V (Ʌ b) ⇒ (a Ʌ c) V (a Ʌ b) here we end only. Only associative property is applied.

    ㄱRoman (x) V ㄱknow (x, marcus) ㄱ hate (x, Caesar) V ㄱhate (y, z) V the thinkcrazy (x, y)

 

8) Create a separate clause corresponding to each conjunction. In order to prove wff to be true, all the clauses that are generated-from it must be true. If we are going to work with several wffs all the clauses generated by each of them can now be combined to represent the same set of facts as were represented by the original wffs. 

    Standardize a part of the variables in the set of clauses in step(8). By this we mean rename the variables. So that no two clauses make, reference to the same variable.. 

    ∀x : P(x) Ʌ Q(x) = ∀x : P(x) Ʌ v ∀(x) : Q(x).