Variables in Hypotheses

1 Introduction

We consider here the problem of checking the consistency of a the­ ory generated by a program. We consider the problem in terms of a theory formation system which has a fixed set of possible hypotheses (i .e., we are assuming some other system is supplying the general forms we can to assume . This study is independent of how the possible hypotheses are generated) . This is a problem because variables in a generated theory somehow need to have their quantification reversed when checking consistency. This paper shows that some proposed solutions do not work, and pro­ vides a solution to the problems where we don't allow variables in our hypotheses, and the general case where we allow arbitrary instances of defaults. ·

2 Formal Semantics

We use the standard syntax of the first order predicate calculus, with variables in upper case. We assume we have the following two sets of formulae:

F is a set of closed formulae (called facts) , which we are given as true

ll is a set of formulae, each instance of which can be used as a possible hypothesis

We say formula g is explainable if there is some D, a set of in­ stances of elements of ll, such that

F U D is consistent

Variables in Hypotheses

David Poole Logic Programming and Artificial Intelligence Group, Department of Computer Science, University of Waterloo, Waterloo, Ontario, Canada, N2L3Gl dlpoole@waterloo.csnet

D is said to be the theory that explains g.

Without loss of generality, we assume that g is variable free, and is an atom. We also assume that elements of ll are atomic and do not contain bound variables. These assumptions do not restrict the expressiveness of the system, but make analysis sim­ pler.

N.B. w E ll is equivalent to [Reiter80]'s normal default : Mwj w [Poole86]

3 Implementation

The obvious way to implement explainability [Reiter80,PGA87] is to note that both proving the observations, and testing con­ sistency are the role of a theorem prover . Intuitively, the idea is to try to prove the goal from F and ll, and make D the set of instances of ll used in the proof. A complete theorem prover is an appropriate tool to check whether F U D is consistent (by fail­ ing to prove inconsistency) . Checking consistency corresponds to showing that the theory does not predict anything known to be false .

In this paper I assume that we are using some sort of com­ plete resolution theorem prover (see eg. [Chang73]) to generate the instances of hypotheses which imply the goal. The results, however, do not seem to be restricted to such systems:.

There is a problem which arises when there are variables in the D generated. Consider the following example:

Example 1 Let ll = {p(X)} . That is, any instance of p can be used if it is consistent . Let F = {lfY (p(Y) * g), --.p( a)}, that is g is true if there is some Y for which p(Y) is true.

g is explainable with the theory {p(b)}, which is consistent with F (consider the interpretation I = {--.p(a),p(b)} on the domain {a, b}), and implies f . So according to our semantics above, g is explainable.

However, if we try to prove g, we generate D = {p(Y)} where Y is free (implicitly a universally quantified variable). The ex­ istence of the fact --.p(a) should not make it inconsistent, as we want g to be explainable.

Theorem 1 In proving ezplainability, it is not adequate to only consider interpretations in the Herbrand universe of 6ome set of formulae .

Proof consider the example above; the Her brand universe is just the set {a} . Within this domain there is no consistent theory to explain g. 0

This shows that Herbrand's theorem is not applicable to the whole system. It is, however, applicable to each of the deduction steps [Chang73] .

4 Ground Instances of Defaults

Consider first the case where we only allow ground instances of po88ible hypotheses in a theory. A ground instance is defined to be one without variables or Skolem constants.

The procedure 1 to compute explainability, when we only al­ low ground instances of defaults in theories, is

1. Skolemise F, forming F,k (free variables are universally quantified);
2. try to prove g using elements of F,k and a as axioms. Make Do the set of instances of a used in the proof;
3. reject Do if it contains a Skolem function (that is try to find another proof of g);
4. Form D1 by replacing free variables in Do with unique con­ stants;
5. add D1 to F and try to prove an inconsistency. If complete search for a proof fails, g is explainable.

Example 2 consider F and a as in example 1 above. If we try to prove g, we use the hypothesis instance p(Y). This means that g is provable from any instance of p(Y). To show g cannot be explained, we must show that all ofthe instances are inconsistent. The above algorithm says we replace Y with a constant {3. p(/3) is consistent with the facts, so that we can show g is explainable.

Let us first try to justify this procedure.

If g is explainable, there is a ground theory D which explains g. Some more general set Do of instances of defaults can be generated in the manner described above such that D = Do9 for some 9 (this is a direct corollary of the lifting lemma [Chang73, page 84]) .

The thitd step of the procedure enforces the groundne88 of defaults found . The fourth and fifth steps follow from checking if 3X Do is consistent by Skolemising the X (the free variables in Do).

6 Arbitrary Instances of Defaults

Sometimes we don't want to be restricted to just ground instances of defaults. Consider the following examples:

Example 3 Consider the blocks world, where we only want pos­ itive knowledge about which blocks are on each other, and we want the closed world assumption for "on" . This is done by hav­ ing the defaults: a= { -.on(X, Y)}.

If we have

This says that a block has a clear top if there is nothing on it, and that block a is on block b. We want to conclude that b does not have a clear top, and all other blocks have a clear top.

1 Thio problem io, in gener,.l, undecidable; this procedure h:.e the property that if it halts, it has computed a correct anewer, and if a provable answer exists this (nondeterministic) procedure can compute it.

Example 4. Let a = {ontable(X)} . That is, we may &~~~~ume that any block is on the table. Let

We want to say that g is explainable as there is a red thing on the table, namely the object that we know is red (but do not know its name). The ground procedure would reject such an answer, as it must know the name of the individual said to exist.

We extend the definition of explainability to allow arbitrary instances of the possible hypotheses in our theories. In particular we want to be able to &!Illume a default for all individuals we can.

If we want to expand the procedure given in the previous section, we have to consider how to handle existentially quantified variables. The standard way to do this is to give names to the individuals said to exist (i.e. Skolemisation, [Chang73]) . If we Skolemise it allows us to use normal resolution theorem provers. However, we must consider the Skolem functions in the theories generated.

It has been suggested [Bledsoe78,Cox84] that we "reverse Skolemise" the generated hypotheses. If we can prove their nega­ tion, we have shown the theory inconsistent; if a complete theo­ rem prover fails to prove their negation the theory is consistent. This is equivalent to unifying the reverse Skolemised form with provably inconsistent instances of possible hypotheses.

Unfortunately, no such pattern matching program will work in general.

Theorem 2 There can be no algorithm which doea pattern match­ ing on the in11tancea which lead to the goal to be e:r:plained, and the inatancea which are inconaiatent auch that the goal ia ezplained if and onl11 if the pattern matcher faila.

Proof: To prove this it is adequate to show two examples which have identical inconsistent hypotheses and syntactically identical instances which can prove the goal, but have opposite answers.

The examples we use are based on having just one simple default, namely that any individual is in the table: Consider a = { ontabl e( X)} and

That is, there is one block (a) that is not on the table, and is red. g 1 is explainable if everything is on the table. 92 is explainable if all non-red things are on the table. According to our semantics g1 should not be explainable (as we can't assume a is on the table), but g2 should be explainable (assuming that everything except a is on the table).

When attempting to compute their explanations, we note that exactly the same instances of hypotheses lead to each goal, and exactly the same instances are inconsistent. Put into Skolem normal form this becomes:

To prove each g; we generate the theory { ontable(c;)}, and the only inconsistent instance of hypotheses is ontable(a) . Note that the last clause is not used in either the proof of g2 nor in

6 Building the Knowledge Base

The problem we have is that we have lost the context of what the Skolem constants represent. In this section we show how Hilbert's e-symbol can be used to keep track of which functions the Skolem functions denote.

Hilbert's e-symbol is a notational device to implicitly describe an individual said to exist. ex.P(x) is, intuitively "an x such that P( x) is true" . This was designed to eliminate existential variables through the equivalence:

where w[X] is any well formed formula parameterised by X . See [Leisenring69] for a detailed description of Hilbert's e-symbol.

When Skolemising (see [Chang73]), we replace

(where w[X11 .. . , X,., Y] is a well formed formula with free vari­ ables X1, .. . ,X,., Y) with

We should also define what f is. We can use Hilbert's e-symbol to define /:

that is

To build the knowledge base, Skolemise all existentially quan­ tified variables, and record the definitions of all Skolem functions and constants. In the Skolemised form all variables are univer­ sally quantified and so explicit quantification can be removed.

7 The General Explanation Procedure

The procedure outlined here is an extension of the one presented in section 4. See [Poole87] for more details.

We are trying to solve the problem of given some g, whether it is explainable or not. That is, if there are assumptions from d which can be consistently added to F to imply g.

The following describes the algorithm:

Let F,~c be the Skolemised form of facts F. We assume we have recorded the definitions of all Skolem functions.

Try to prove g from F,~c and d. Let Do be the set of instances of elements of d used in the proof.

Let D1 be a grounding of Do. That is, we replace free vari­ ables in Do with unique constant symbols. We then know

by construction (given our proof procedure is sound).

Form D2 by replacing each instance of a Skolem function /;(tl, ... , t,.) (where/; = At11 ... Av,.ey.w;[v1, .. . , v,., y]) in D1 with a unique variable x;. We know (lfx1, ... , lfx,. D2[x1, ... , x,.]) implies D1 and does not contain any Skolem functions, and so

We now find out which instances of D2[x11 .. . , x,.] we cannot assume. To do this, we try to prove ..,D2[x11 ... , xm] from F,~c. We collect up the instances of the x; proven [Green69]. Suppose we find the answer 2 :

We know that we cannot assume any instance of D2[c1, .. . , em] ·

For those instances which we need in the above proof that we cannot use (because they are inconsistent), we must find an alternate explanation. The instances we need for the proof of g are for x; = f;(tl. ... ,t,.) = ey.w;[t1, ... ,t,.,y] The ones we must reexplain are where x;=c; (for every instance of c;). That is, for the case w;[t11 .. . , t,., c;] we must find an alternate proof to that found initially (for all instances of the c;) .

For each inconsistency of the above form found, we must try to reexplain g from the case

If F' is consistent, then we can explain g only if we can explain g (using a different set of instances of elements of d) from F'. If F' is inconsistent, then inconsistency found is irrelevant to the theory needed to explain g.

In this description, we have ignored the problems of Skolem functions appearing in the c; and the t;, as well as disjunctive answers from the proof of ..,D2. See [Poole87] for full details.

Example 5 Consider the blocks world of example 3. Let

d = {-,on( X, Y)}

That is, we can explain 9b if b has a clear top, and explain fc if c has a clear top.

Skolemising the facts gives,

We can prove 9b generating the theory Do = {-,on(!( b), b)}. D1 =Do. The corresponding D2 = {..,on(Y,b)}. We then try to generate all answers to on(Y, b), which is provable (Y =a) .

We then try to reexplain g making a = f (b) = e Y. -,on(Y, b) => cleartop(b), that is we try to explain g (using an alternate proof to above) from

which cannot be done.

We can explain 9c as we cannot prove the negation of the corresponding D2, that is we cannot prove 3Y on(Y, c) .

'If w lo a. formula, Vw Ia the unlvenal clooure of w. That io if w ha.o free varlableo v1, ... ,v. then Vw is defined to be Vv, ... Vvo w. Similarly 3w is defined to be the existential closure of w.

Example 6 Consider the example in theorem 2 above. The Skolem constants, c; have different definitions,

In each case the generated theory is Do = { ontable(c;)} . So for each of these we have D2 = {ontable(X)} . We try to prove

This can be proven, in each case, for X= a.

In the first case, we then have to explain g1 from

which cannot be done (using a different theory) . Hence g1 cannot be explained.

To prove the second case inconsistent, we have to explain g2 from

that is, we have to try to explain g2 from

This can be done (as red( a) is in F) . Thus g2 can be explained.

Example 7 Consider example 4. t. = {ontable(X)}.

Skolemised, the facts become,

where c = EX.red(X). We can explain g, generating Do = {ontable(c)} which gives D2 = {ontable(X)} . We cannot prove -,ontable(X) for any X, so that g is explained.

Example 7A Let F1 = FU{red(a),...,ontable(a)} . g should not be explainable from F1, as there is no reason to assume that there is another individual which is also red. We can prove, -,ontable(X) for X = a and cannot explain g from FA red( a) .

Example 7B Let F2 = Fu {-,red( a), -,ontabl e( a)}. g should be explainable from F2, as we know there is another individual which is red which we can assume is on the table. We can explain g with the same theory, we can prove -,ontable(X) for X = a, but F' = F A red( a) is inconsistent, and so the inconsistency is irrelevant to the theory needed.

8 Conclusion

There are many areas in which this problem arises. Some people have assumed that it is sufficient to consider the Herbrand Uni­ verse [Reiter80] . Others have tried to define a "reverse Skolemi­ sation" algorithm which can be applied to the hypotheses gen­ erated, and unified with the instances leading to inconsistencies [Cox84,Bledsoe78] . We have shown that both of these ideas can­ not work.

We have shown that we need to keep track of the context in which Skolem functions are defined, and have shown how this can be done by using Hilbert's £-symbol. A procedure is outlined which solves this problem for the case of no Skolem functions in the inconsistencies found . [Poole87] gives the general solution to the problem.

Acknowledgements

This research was supported under NSERC grant A6260. Thanks to Eric Neufeld, Paul Van Arragon, Denis Gagne, Bruce Kirby and Randy Goebel for valuable discussions, arguments and com­ ments on an earlier draft of this paper .