Artificial Intelligence
Prof. R. Williams


			      SKOLEMIZATION


The objective of skolemization is to end up with a form having no explicit
quantifiers.  The basic idea is to have universally quantifiers appropriately
flagged and to have existentially quantified variables replaced by what are
called Skolem functions.  Before this step is performed, however, it is
generally necessary to transform the original formula in certain ways.

Here we look at a version of skolemization appropriate for forward and
backward chaining, in which it is desirable to preserve the implications
originally present in the formula to be skolemized.  The simple algorithm
to be described below (which is used in the "skolemize" function found in
the file "skolemize.lisp") works because it amounts to performing the
following equivalence-preserving transformations:

1.  Standardize variables apart.  This means to rename some of the dummy
variables if necessary to insure that each quantifier has its own unique
dummy variables.

For example,

    (or (forall (x) (exists (y) (P x y)))
        (forall (y) (exists (x) (Q x y))))

should be transformed to

    (or (forall (x) (exists (y) (P x y)))
        (forall (z) (exists (w) (Q w z))))

2.  Move all quantifiers ("forall" and "exists") outside of negations ("not")
and antecedents of implications ("if").  The relevant transformations are based
on the following logical equivalences:

  a. (and (forall (x) (P x)) q)  is equivalent to    (forall (x) (and (P x) q))
  b. (and (exists (x) (P x)) q)  is equivalent to    (exists (x) (and (P x) q))
  c. (or (forall (x) (P x)) q)   is equivalent to    (forall (x) (or (P x) q))
  d. (or (exists (x) (P x)) q)   is equivalent to    (exists (x) (or (P x) q))
  e. (not (forall (x) (P x)))    is equivalent to    (exists (x) (not (P x)))
  f. (not (exists (x) (P x)))    is equivalent to    (forall (x) (not (P x)))
  g. (if p q)                    is equivalent to    (or (not p) q).

This last equivalence is the reason that the antecedent of an implication is
treated as being negated when applying the algorithm used in the "skolemize"
function.  In fact, we can derive the following four equivalences dealing
specifically with implications from equivalences (c)-(g) above:

  h. (if (forall (x) (P x)) q)    is equivalent to   (exists (x) (if (P x) q))
  i. (if (exists (x) (P x)) q)    is equivalent to   (forall (x) (if (P x) q))
  j. (if p (exists (x) (Q x)))    is equivalent to   (exists (x) (if p (Q x)))
  k. (if p (forall (x) (Q x)))    is equivalent to   (forall (x) (if p (Q x)))

In general, we transform our original formula by a sequence of transformations
in which any expression having the form of the left-hand side of any of the
equivalences (a)-(f) or (h)-(k) is replaced by the appropriate version of
the corresponding right-hand side.  The objective is to obtain a logically
equivalent formula in which each quantifer is no longer in the scope of any
negations or implication antecedents.  The key transformations are thus
(e), (f), (h), and (i), which may be summarized as the rule that each time a
quantifier is moved outside a negation or implication antecedent it changes
from being a universal to an existential quantifier and vice versa.

For example,

  (not (forall (x) (exists (y) (P x y))))

becomes

  (exists (x) (forall (y) (not (P x y))))

and

  (forall (x) (if (exists (y) (P x y)) (Q x)))

becomes

  (forall (x) (forall (y) (if (P x y) (Q x))))

which we can also write as

  (forall (x y) (if (P x y) (Q x))).

The use of any of the other transformations listed above merely serve to
aid in the process of moving quantifiers outside negations and implication
antecedents.  In some cases, the use of other well-known equivalence-preserving
transformations may also be required.  For example, to move the quantifiers
outside the negation in

  (not (or (forall (x) (P x)) (exists (y) (Q y)))),

we must apply one of de Morgan's laws to transform this to

  (and (not (forall (x) (P x))) (not (exists (y) (Q y)))),

which is then transformed to

  (and (exists (x) (not (P x))) (forall (y) (not (Q y)))).

Once we have a logically equivalent formula in which no quantifer is in the
scope of any negation or implication antecedent, we then do the following:

3.  Eliminate existential quantifiers ("exists") and replace the corresponding
variables with Skolem functions.  Each Skolem function must have as its
arguments all universally quantified variables that are bound by universal
quantifiers ("forall") whose scopes include the scope of the existential
quantifier being eliminated.  This includes the case where an existential
quantifier being eliminated is not within the scope of any universal
quantifiers, in which case we use a Skolem function of no arguments, which
is just a constant.

For example,

  (exists (x) (forall (y) (not (P x y))))

becomes

  (forall (y) (not (P sk-1 y))),

where sk-1 is a Skolem constant (function of no arguments), and

  (forall (x) (exists (y) (not (P x y))))

becomes

  (forall (x) (not (P x (sk-2 x)))),

where sk-2 is a Skolem function of one argument.

4.  Eliminate universal quantifiers ("forall").  This leads to a formula whose
interpretation follows the convention that all unbound variables are implicitly
taken to be universally quantified.  In order to make clear just which symbols
represent these implicitly universally quantified variables, we prefix them
with "?".

For example,

  (forall (x) (not (P x (sk-2 x))))

becomes

  (not (P ?x (sk-2 ?x))),

and

  (or (forall (x y) (P x y (sk-17 x)))
      (forall (z) (Q z)))

becomes

  (or (P ?x ?y (sk-17 ?x))
      (Q ?z)).

It should now be clear why it is necessary to standardize variables apart.

Now let's consider an example where we start with the English sentence

  "Any box not having another box on top of it is liftable."

We might translate this into the predicate calculus formula

  (forall (x) (if (and (box x)
                       (not (exists (y) (and (box y)
	  				     (on-top-of y x)))))
		  (liftable x)))

Since the variables are already distinct, we begin by moving the existential
quantifier outside of the negation and implication antecedent.  To do this,
we transform the above formula to

  (forall (x) (if (and (box x)
		       (forall (y) (not (and (box y)
					     (on-top-of y x)))))
		  (liftable x)))

and then to

  (forall (x) (if (forall (y) (and (box x)
		       		   (not (and (box y)
					     (on-top-of y x)))))
		  (liftable x)))

and finally to

  (forall (x) (exists (y) (if (and (box x)
		       		   (not (and (box y)
					     (on-top-of y x)))))
		  (liftable x))).

Eliminating the existential quantifier and replacing its variable y by a
Skolem function, we get

  (forall (x) (if (and (box x)
		       (not (and (box (sk-13 x))
				 (on-top-of (sk-13 x) x))))
		  (liftable x))).

Finally, we eliminate the universal quantifier and prefix its variable x
with "?" to obtain

  (if (and (box ?x)
           (not (and (box (sk-13 ?x))
	             (on-top-of (sk-13 ?x) ?x))))
      (liftable ?x)),

the skolemized version of our original formula.



		A Simple Algorithm for Skolemization
		------------------------------------

It is really not necessary to perform all the logical transformations of the
original formula when performing skolemization.  It is really only necessary
to determine how many negations and implication antecedents each quantifier
is contained in the scope of.  Whenever it is an even number, that quantifier
stays the same; whenever it is an odd number, it switches to the other type.
The reason is that whenever a quantifier is moved outside of any negation,
whether explicit ("not") or implicit (antecedent of "if"), it switches to
the other type.  Thus an even number of switches turns it into the same
type while an odd number turns it into the other type.  Here is how this
simple algorithm works on some examples:

Example 1. "Everybody loves somebody."

   (forall (x) (if (person x)
		   (exists (y) (and (person y) (loves x y)))))

The "forall" quantifier is outside the scope of anything else, so the
variable x remains universally quantified.  The "exists" quantifier is
not inside the scope of any "not" or "if" antecedent, so the variable y
remains existentially quantified.  (Note that the "exists" is inside the
scope of the consequent of the "if", but this does not affect anything.)
Thus we replace x by ?x and we replace y by a Skolem function.  Since y
is introduced inside the scope of the universally quantified variable x,
the corresponding Skolem function must be a function of ?x.  Thus the
skolemized version of this is

   (if (person ?x)
       (and (person (sk-421 ?x)) (loves ?x (sk-421 ?x))))

We might have called sk-421 the "a-person-loved-by" function.

Example 2. "There is somebody who is loved by everybody."

   (exists (x) (and (person x)
		    (forall (y) (if (person y) (loves y x)))))

Neither of the two quantifiers is inside the scope of any "not" or
"if" antecedent, so x is existentially quantified and y is universally
quantified.  Since x is introduced outside the scope of any universal
quantifiers, its Skolem function is a function of no arguments, i.e.,
a constant.  The skolemized version of this is thus

  (and (person sk-39) (if (person ?y) (loves ?y sk-39)))

The Skolem constant sk-39 can be thought of as a name we have made up to
identify this person who is loved by everybody.

Example 3. "Any box not having another box on top of it is liftable."

  (forall (x) (if (and (box x)
                       (not (exists (y) (and (box y)
	  				     (on-top-of y x)))))
		  (liftable x)))

The "forall" is not in the scope of any "not" or "if" antecedent, so x
remains universally quantified in the skolemized version, becoming ?x.
The "exists" is inside the scope of the "not" and the antecedent of the "if".
Since this would give an even number of switches, y remains an existentially
quantified variable.  The corresponding Skolem function must be a function
of ?x because it is introduced inside the scope of this universally quantified
variable.  The skolemization is thus

  (if (and (box ?x)
	   (not (and (box (sk-5 ?x))
		     (on-top-of (sk-5 ?x) ?x))))
      (liftable ?x))

This is (essentially) the same result obtained above for this example by
laboriously transforming the formula using the appropriate
equivalence-preserving transformations.

Example 4. "Any box having another box on top of it is not liftable."

  (forall (x) (if (and (box x)
                       (exists (y) (and (box y)
	  				(on-top-of y x)))))
		  (not (liftable x)))

The "forall" is not in the scope of any "not" or "if" antecedent.
The "exists" is inside the scope of the antecedent of the "if", so y
switches to a universally quantified variable.  The skolemization is
then

  (if (and (box ?x)
	   (and (box ?y)
		(on-top-of ?y ?x)))
      (not (liftable ?x)))

We can simplify this slightly to

  (if (and (box ?x)
	   (box ?y)
	   (on-top-of ?y ?x))
      (not (liftable ?x)))

Note that this is also the skolemization of

  (forall (x y) (if (and (box x)
		     	 (box y)
			 (on-top-of y x))
		    (not (liftable x))))

which corresponds essentially to the English sentence

  "Whenever there is a pair of boxes with one box on top of the other,
   the box underneath is not liftable."

which is clearly logically equivalent to the original sentence.