Converting Arbitrary wffs to Clause Form in Artificial Intelligence

Converting Arbitrary wffs to Clause Form 

The wffs in predicate calculus can be converted into clause forms. 

The steps involved are as follows, 

1) The implication signs are to be eliminated. 

2) The scope of negation signs must be reduced. 

3) Variables should be standardized. That is, by renaming. 

        Example: (∀y) (ᆨP(y) ∨ (∃y) Q(y)] have to be written as (∀y) [(ᆨP(y) ∨ (∃x) Q(x)]. 

4) Existential quantifiers must be, eliminated. 

        Example: Let us consider (∀x) [(∃y) Weight(x, y)] 

    In the example the existential quantifier is ,with in the scope of universal quantifier so the value of y may depend on value of x. 

• Let us assume that x is a child and has a weight y. The weight obviously depends on child, so let us denote this relation as w(x), where x is mapped into y that exists. 
• Skolem Function: The w(x) Which we defined above- is known as a skolem function. 
• By replacing y -with skolem function we have (∀x) Weight[x, w(x)] where we eliminated existential quantifier. 
• Tile symbols used for representing skolem functions must "new" i.e., they should not be present in the expressions before.
• In the cases where the existential quantifier is out of the scope of universal quantifier skolem function of no arguments is used that is a constant. 
• Example: (∃x) (Q(x)) will become Q(sk), Where constant sk is known to exist. 
• Here, sk should be a new symbol it should not be present in the expressions used 
• Skolem Form: The form of expression obtained by eliminating all the existential quantifiers is known as skolem form.
• This skolem form is not similar to original wff but it logically entails the formula, 
• i.e. P(sk) |== (∃x) P(x) and [P(A) ∨ P(B) |== (∃x) P(x) but [P(A) ∨ P(B)] ⊭ P(sk)) 

5) Then it is converted to prenex form. 

• As there are no existential quantifiers making the scope of universal quantifier to apply to entire wff has to be done. This form is known as prenex form.
• In this form the wff has a prefix and it is followed by a formula which does not contain any quantifiers called a matrix. 

            Example:

6) The next step is to convert the matrix into conjunctive normal form by using distributive rules. 

7) Now, the universal quantifiers have to be eliminated. Since the whole expression is in the scope of universal quantifiers and the order of application of them is not important we eliminate them and left with matrix which is in conjunctive normal form. 

8) Now the '∧' conjunctive symbols are to be eliminated. 

• These symbols are eliminated by replacing the wffs of the form (w₁ ∧ w₂) as {w₁, w₂}. 
• After replacing, we have a finite set of wffs where each of them are disjunction of literals. 
• A wff which consists of only a disjunction of literals is called a clause. 

            Now the matrix is converted into, 

                ᆨQ(x) ∨ ᆨQ(y) ∨ Q(f(x, y)) 

                ᆨQ(x) ∨ P(x, w(x)) and 

                ᆨQ(x) ∨ ᆨQ(w(x)) 

9) The final step is to rename the variables. The renaming is done as that in every clause there are different variables. 

                ∴ Now we have, 

                ᆨQ(x₁) ∨ ᆨQ(y) ∨ Q(f(x₁, y)) 

                ᆨQ(x₂) ∨ Q(x₂, w(x₂)) and 

                ᆨQ(x₃) ∨ ᆨQ(w(x₃)) 

The literals of a clause are always considered as universally quantified. 

Fig: Steps in Converting Arbitrary wff to Clause Form in Predicate Calculus