Conversion to the canonical form

To put axioms into conjunctive normal form (clause form):

  1. eliminate implications

  2. move negations down to the atomic formulas

  3. purge existential quantifiers

  4. rename variables if necessary

  5. move the universal quantifiers to the left

  6. move the disjunctions down to the literals

  7. eliminate the conjunctions

  8. rename the variables if necessary

  9. purge the universal quantifiers

Consider the following example. Suppose we assert that ``all musiclovers who enjoy Bach either dislike Wagner or think that anyone who dislikes any composer is a philistine''. We shall use enjoy() for enjoying a composer, and similarly for dislike.

"x[musiclover(x) enjoy(x,Bach)
    dislike(x,Wagner) ( "y[$z[dislike(y,z)] =>think-philistine(x,y)])]
We now examine the recipe to reach the conjunctive normal form needed in resolution. It is rather long, but not difficult to follow, and should give confidence in handling expressions.

Step 1: Recall that E F E F, and thereby filter the expression to remove symbols.

"x [ (musiclover(x) enjoy(x,Bach)) =>
    dislike(x,Wagner) ( "y[ $z [dislike(y,z)]=> think-philistine(x,y)])].

Step 2: Filter using the following relationships:

( P) <=> P;
( ab ) <=> a b;
( a b ) <=> a b;
"x P(x) <=> $x P(x); and
$x P(x) <=>"x P(x).
Our expression becomes
"x[ musiclover(x) enjoy(x,Bach)
    dislike(x,Wagner) "y[ "z[dislike(y,z)] think-philistine(x,y)]].

Step 3: Standardize variables so that each quantifier binds a unique variable. This is already the case in our expression, but the following is an example.

"x Pred1(x)"x Pred2(x)
becomes
"x Pred1(x) "y Pred2(y).

Step 4: Step 3 allows us to move all the quantifiers to the left in Step 4. Our expression becomes

"x"y"z[ musiclover(x) enjoy(x,Bach)
    dislike(x,Wagner) dislike(y,z) think-philistine(x,y)].
This is called the prenex normal form.

Step 5: This step will seem a bit of a fiddle. We eliminate existential quantifiers, by arguing that if

$y Composer(y)
then if we could actually find an Object S1 to replace the Variable x. So this gets replaced simply by
Composer(S1).
Now, if existential quantifiers exist within the scope of universal quantifiers, we can't use merely an object, but rather a function that returns an object. The function will depend on the univeral quantifier.
"x$y tutor-of(y,x)
gets replaced by
"x tutor-of(S2(x),x).

This process is called Skolemization, and the S2 is a Skolem function.

Step 6: This step is merely to save writing. Any variable left must be universally quantified out on the left, so don't bother writing the quantifier. Our expression becomes:

musiclover(x) enjoy(x,Bach)
    dislike(x,Wagner) dislike(y,z) think-philistine(x,y).

Step 7: Convert everything into a conjunction of disjunctions using the associative, commutative, distributive laws. The form you want is like:

(a b c d ...) ( p q ...) ...

Step 8: Call each conjunct a separate clause. In order for the entire wff to be true, each clause must be true separately.

Step 9: Standard apart the variables in the set of clauses generated in 7 and 8. This requires renaming the variables so that no two clauses make reference to the same variable. Remember that all variables are implicitly universally quantified to the left.

"x P(x) Q(x) <=> "xP(x) "xQ(x) <=> "xP(x) "yQ(y)

This completes the recipe. After application to a set of wffs, we end up with a set of clauses each of which is a disjunction of literals.

<<<Previous Next>>>