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.