Model Elimination, Logic Programming and Computing Answers

1 From Tableau to Restart Model Elimination

1.1 Tableau Model Elimination

In this subsection we use the clause notation, mirroring the fact that we review a calculus which is, as it stands, not suited for programming purposes. We use a ME calculus that differs from the original one presented in [Loveland, 1968]. It is described in [Letz et al., 1992] as the base for the prover SETHEO. In [Baumgartner and Furbach, 1993] this calculus is discussed in detail by presenting it in a consolution style [Eder, 1991] and compared to various other calculi. ME (in this sense) manipulates trees by extension and reduction steps. In order to recall the calculus consider the clause set

A model elimination refutation is depicted in Figure 1 (left side). It is obtained by successive fanning with clauses from the input set (extension steps). Additionally, it is required that every inner node is complementary to one of its sons. Such sons are decorated with a "*" in Figure 1. A dashed arrow indicates a reduction step, i.e. the closing of a branch due to a path literal complementary to the leaf literal. Extension and reduction steps are allowed at any leaf of the tree and for extension steps any literal from an input clause can be used to form a complementary pair of literals. For example, in the right subtree of Figure 1 (left side) the clause { ....,p, Q} was used to extend the positive leaf P, i.e. we used the program clause Q +- P via the body literal P and hence did dissent with a procedural reading of the clause.

In the right part of Figure 1 a refutation with the modi­ fied version, the restart ME calculus, is displayed. The only difference is that extension steps at positive literals are not allowed; instead either a reduction step is carried out, or else the root literal - which is always -,goal - is copied, and then an extension follows.

In a variant called strict restart model elimination not even reduction steps are allowed at positive leaves. Hence the cal­ culus is forced to apply restart steps wherever possible.

These simple modifications obviously allow only exten­ sion steps with a positive, i.e. a head literal of a clause, and hence support a procedural reading of program clauses. In the following subsection we give a formal presentation of the calculus along the lines of [Baumgartner and Furbach, 1993].

1.2 Restart Model Elimination

Instead of trees we now manipulate multisets of paths, where paths are sequences of literals. We will state some basic defi­ nitions.

A clause is a multiset of literals, usually written as the dis­ junction LtV . . . V Ln. Aprogramis a consistent set of clauses (thus possibly including negative clauses). A connection is a pair of literals, written as (K, L), which can be made com­ plementary by an application of a substitution. A path is a sequence of literals, written asp = (Lt , . . . , Ln) . Ln is called the leaf of p, which is also denoted by leaf(p ); similarly, the first element Lt is also denoted by first(p ). The symbol "o" denotes the append function for literal sequences.

In the sequel both path sets and sets of literals are always understood as multisets, and usual set notation will be used. Multisets of paths are written with caligraphic capital letters.

From now on we use the notation At V . .. V Am +- E1 A ... A En as a representation of the clause At V . . . V Am V ....,Et V . . . V ...,En. Such clauses are called program clauses with head literals Ai (if present) and body literals Ei .

We assume our clause sets to be in goal normal form, i.e. there exists only one goal clause (a clause containing only negative literals), which furthermore does not contain variables. Without loss of generality this can be achieved by introducing a new clause +- goal where goal is a new predicate symbol, and by modifying every purely negative clause ....,Et V . .. V -,En to goal+- Et, . .. , En .

If C = At V .. . V Am +- Et A ... A En is a clause then its path set Pc is {(L) I L E {At, . .. , Am, -,Et, ... , -,En}}. The dot product p · Q of a path p and a path set Q is defined as {p o q I q E Q}. It can be interpreted as a branching of a path p into the new paths from Q

The inference rule extension from the restart ME calcu­ lus, will be defined in such a way that one is free in selecting any head literal as part of a connection. For this, we introduce a head selection function. ·

Definition 1.1 (Head selection Function) A head selection function! is a function that maps a clause At V . .. VAn +­ Bt A . . . A Bm with n ~ 1 to an atom L E {At , ... ,An}· L is called the selected literal of that clause by f . The head selection function/ is required to be stable under lifting which means that iff selects Vy in the instance of the clause (A 1 V ... VAn +- Bt A ... A Bmb (for some substitution 'Y) then/ selects Lin At V .. . VAn +- Bt A .. . A Bm. (End Definition)

Note that this head selection function has nothing to do with the selection function from SLD-resolution which selects subgoals. This will be discussed later.

Definition 1.2 (Strict Restart Model Elimination) Given a set of clauses S and a head selection function.

The inference rule extension is defined as follows:

where

1. P U {p} is a path multiset, and A 1 V ... VA; V . .. V Am +­ Bt A .. . A Bn is a variable disjoint variant of a clause in S; A; is the selected literal, and
2. (leaf(p),A;) is a connection with MGU a, and

The inference rule reduction is defined as follows:

1. P U {p} is a path multiset, and
2. there is a positive literal Lin p such that (L, leaf(p)) is a connection with MGU a.

The inference rule restart is defined as follows:

1. P U {p} is a path multiset, and

1. leaf(p) is a positive literal, and
2. L = first(p ).

A strict restart ME derivation from the clause setS consists of a sequence (Po, P1, ... , Pn) and a substitution u1 · · · Un, where

1. Po is a path multiset { (L1), ... , (Ln)} consisting of paths of length 1, with L1 V ... V Ln in S (also called the goal clause), and fori= 1 ... n
2. P; is obtained from P;-1 by means of an extension step with an appropriate clause C from Sand MGU u;, or
3. P; is obtained from P;-1 by means of a reduction step and MGU u;, or
4. P; is obtained from P;-1 by means of a restart step.

The path p is called selected path in all three inference rules. A restart step followed immediately by an extension step at the just obtained path is also called a restart extension step. Finally, a refutation is a derivation where Pn = {}. (End Definition)

Note that in extension steps we can connect only with the head literals of input clauses. Since in general this restriction is too strong, we have to "restart" the computation with a fresh copy of a negative clause. This is achieved by the restart rule, because refutations of programs in goal normal form al­ ways start with -,goal, i.e. the copied literal.first(p) = -,goal; furthermore, only extension steps are possible to -,goal, in­ troducing a new copy of a negative clause (cf. Figure 1, right side).

The reduction operation is permitted from negative leaf lit­ erals to positive ancestor literals only. This condition can be relaxed towards disregarding the sign, which then yields the non-strict calculus version. See [Baumgartner and Furbach, 1994a] for a discussion of the differences. The reader aware of this work will notice that in the present text we define the cal­ culus slightly different. This happens in order to conveniently express another calculus variant defined below.

Note that the restart ME calculus does not assume a special selection function which determines which path is to be ex­ tended or reduced next. Correctness and completeness of this calculus follows immediately from a result in [Baumgartner, 1994]. From the definition of the inference rule extension, it follows immediately, that this calculus only needs those con­ trapositives of clauses which contain a positive literal in their heads.

2 Computing Answers

In this section we introduce the notion of computed answers and we state an answer completeness result for restart ME. We assume as given a program P together with one single query +-- G1 /1. · · · /1. Gn , where the Gis are positive literals. We will often abbreviate such a query as - Q, where Q stands for the conjunction of Gis. The clause set S is the transforma­ tion of P U {- Q} into goal normal form. In the following definition of computed answer we collect applications of the query clause, but not applications of negative clauses from the program P.

Definition 2.1 (Answers) If - Q is a query and fh, ... , Om are substitutions for the variables from Q, then Q()1 V ... V Q()m is an answer (for S). An answer Q01 V .. . V QOm is a correct answer if P F V(Q01 V ... V QOm). Let now a restart ME refutation of S with goal clause - goal and substitution u be given. Assume that this refutation contains m extension steps with the query, i.e. it contains m-times an extension step with the clause goal- Qp;, where p; is the renaming substitution of this step. Let u; = p;uldom(p;) · Then Qu1 V ... V Qum is a computed answer (for S). (End Definition)

Theorem 2.2 (Lifting Theorem for Restart Model Elimi­ nation) Let S' be a set of ground instances of clauses taken from a clause set S. Assume there exists a restart ME deriva­ tion D' = PQ, pt, ... , P',. from S' with goal clause CO E S'. Then there exists a restart ME derivation D = Po, P1, . . . , Pn from S with some goal clause Co E Sand substitution u such that Pn is more general than P',.. (A path set Pis more general than a path set Q if! for some substitution 8 we have P8 = Q.)

Furthermore, there exists a substitution 8 such that P'; is obtained from P;_1 by an extension step with clause C' E S' if and only if P; is obtained from P;-1 by an extension step with a clause C E S such that Cpu8 = C', where pis the renaming substitution applied in that extension step.

The first part of the theorem will be used in the proof of refutational completeness (because for a refutation on the ground level, i.e. a derivation of P~ = {},only the empty path set P n = {} can be more general), while the second part will be used in the proof of answer completeness (Theorem 2.3). In particular, to obtain this we have to demand one single substitution 8 which maps any of the clauses Cpu used in extension steps to the respective clause on the ground level. Clearly, this result is harder to establish and more relevant than a lifting result for SLI-resolution in [Lobo et al., 1992] which "moves the 3 quantification inside": in our words, they state that for every application of an input clause at the ground level there exists an application at the first-order level, and there exists a substitution to map this instance to the ground level.

Theorem 2.3 (Answer completeness of restart ME) If Q01 V ... V Q01 is a correct answer for a program P, then there exists a strict restart ME refutation from S with com­ puted answer Qu1 V . .. V Qu m such that Qu1 V ... V Qu m entails Q01 V ... V Q01, i.e.

Informally, the theorem states that for every given correct answer we can find a computed answer which can be instanti­ ated by means of a single substitution 8 to a subclause of the given answer (and hence implies it). Unfortunately we can not obtain a result stating that the computed answer contains less (or equal) literals than the given answer.

All proofs are stated in the long version of this paper [Baum­ gartner et al., 1995].

3 Definite Answers and Regularity

From theorem proving with ME we know that the regularity check is an important means for improving efficiency. Reg­ ularity for ordinary ME means that it is never necessary to construct a tableau where a literal occurs more than once along a path. Expressed more semantically, it says that it is never necessary to repeat in a derivation a previously derived subgoal (viewing open leaves as subgoals).

Unfortunately, regularity is not compatible to restart ME. In this section we will present a variant of restart ME, the ancestry restart variant, which allows for extended regularity checks. This variant is motivated by Loveland's UnH-Prolog [Loveland and Reed, 1992].

As an interesting side effect it turns out that this variant of­ fers considerable benefits with respect to logic programming: occasionally one is interested in the question whether a given program with query admits a definite answer, i.e. an answer which is a single conjunction of atoms, but not a disjunction. Of course, in general, a non-definite program does not always admit a definite answer, but some programs do. It is the latter class of problems we are interested in now.

The key idea to the direct computation of definite answers is to restrict the use of the query to one single application in the refutation, namely at its top. Then, by definition, definite answers are obtained. However, such a restriction is incom­ plete. But if restart ME is modified in such a way that every negative literal along a branch, not only the topmost literal, may be used for the restart step then completeness is recov­ ered. This follows from a more general result which states that we can restrict to globally regular refutations (i.e. no literal except the literal used for the restart occurs more than once along a branch). Let us now introduce all this more formally.

Definition 3.1 (Ancestry Restart Model Elimination) The calculus ancestry restart ME is the same as strict restart ME (Definition 1.2), except that the inference rule restart is mod­ ified by replacing the condition 3. by the new condition 3' .:

3'. Lis a negative literal occurring in p. In this context L is also called the restart literal.

The modified rule is called ancestry restart. (End Definition)

The term "ancestry" in the definition is explained by the use of ancestor literals for restart steps. Note that any reduction from a positive leaf literal to a negative ancestor literal can be simulated in ancestry restart ME by a restart step followed by a strict reduction step. Thus, non-strictness is "built-in" into ancestry restart ME.

Note that the ancestry restart rule includes the restart rule since the first literal can be used for the restart as well.

Clearly, in terms of a proof procedure the ancestry restart rule induces a larger local search space than the restart rule. On the other side, refutations may become much shorter. Indeed, this is the rationale for our proof procedure to search the restart literals from the leaf towards the top. As a further benefit of this search order note that a definite answer will be enumerated before a non-definite answer.

Now we are going towards an appropriate completeness result wrt. definite answers. As mentioned above, this result shall be a consequence of a more general result concerning a regularity restriction. Let us define this notion precisely:

Definition 3.2 (Regularity) Let p be path written as follows (the As and Bs are atoms):

Then p is called blockwise regular iff

1. Ai -:f Ai for 1 ~ i,j ~ n- 1, i -:f j (Regularity wrt. positive literals) and
2. B! # Bj for 1 ~ l ~ n, 1 ~ i,j ~ k,, i =f. j (Regularity inside blocks).

If additionally it holds that

1. B! =f. B'!' for 1 ~ l < m ~ n, 1 ~ i ~ k,, 2 ~ j ~ km (Global negative regularity)

then pis called globally regular. A path set is called (block­ wise, globally) regular iff every path in it is (blockwise, glob­ ally) regular. Similarly, a derivation is called (blockwise, glob­ ally) regular iff every of its path sets is (blockwise, globally) regular. (End Definition)

Condition 1 states that all positive literals along a path are pairwise different, and condition 2 states that negative literals inside blocks are pairwise different, where by a block we mean a smallest subpath delimited by positive literals or the ends of the path. Condition 3 means that a negative literal may be equal to one of its ancestors only if it follows a positive literal, i.e if it is used as a restart literal. Thus we have a global regularity condition, except for restart literals. In all example refutations given so far, all branches are blockwise regular. However, the refutation in Figure 1 (right side) is not globally regular, as can be seen by the two occurrences of .., Q in the rightmost path. From this example we learn that restart ME is incompatible with the global regularity restriction. However it holds:

Theorem 3.3 (Completeness of Ancestry Restart Model Elimination) Let f be a head selection function and S be an unsatisfiable clause set in goal-norma/form. Then there exists a globally regular ancestry restart ME refutation of S starting with .._. goal and selection function f.

We can use this result to obtain the desired completeness result for definite answers.

Theorem 3.4 (Answer completeness of ancestry restart ME) Ancestry restart ME is answer complete in the sense of Theorem 2.3. In particular; if Q(} is a correct definite an­ swer for a program P, then there exists an ancestry restart ME refutation from P with computed answer Qa such that Qa8 = Q(}, for some substitution 8. Furthermore, the input clause goal .._. Q is used exactly once, namely at the first extension step of.._. goal.

The last theorem enables us to enumerate definite answers only, by simply restricting the use of goal .._. Q to one exten­ sion step at the beginning. So we have the desirable properties of loop checking by regularity and the computation of definite answers.

4 Implementation

All variants and refinements of ME discussed so far, i.e. the restart, strict and ancestry variants (possibly with selection function), loop checking by regularity and factorization, are implemented in the PROTEIN system [Baumgartner and Fur­ bach, 1994b]. It is a first order theorem prover based on the Prolog technology theorem proving (PTTP) technique, imple­ mented in ECLiPSe-Prolog.

Since ME is a goal-oriented, linear and answer complete calculus, it is well suited as an interpreter for disjunctive logic programming. PROTEIN facilitates computing disjunc­ tive and definite answers. In its newest release their is also a flag which allows us to look for definite answers only.

S Comparative Theorem Prover Study

In the sequel, we want to tell about our experiences in com­ puting answers by using theorem provers. First of all, we had to overcome some technical problems because theorem provers usually do not supply answers besides "yes" or (pos­ sibly) "no".-We will illustrate our experiences with a puzzle example which allows for indefinite and definite answers.

5.1 Knights and Knaves

The example follows problem #36 in [Smullyan, 1978]. A similar example is studied in [Ohlbach, 19851. The natural language description of the problem is stated below. There, the last two pieces of information 5 and 6 explicitly state some knowledge about inferencing. We need them in order to be able to cope with the information in 2 because our description language is first order. ·

1. On an island, there live exactly two types of people: knights and knaves. 2. Knights always tell the truth and knaves always lie. 3. I landed on the island, met two inhabitants, asked one of them: "Is one of you a knight?" and he answered me. 4. What can be said about the types of the asked and the other person depending on the answer I get?- 5. We assume, that either a proposition or its negation is true. 6. If the disjunction of two propositions is true then at least one of them must be true.

In our formalization of the problem below, the formulae in I and 2 express the corresponding pieces of information from above. Depending on the case considered, we choose one of the formulae (a) or (b) in 3. We view the fact that a person denies a question as that he says that the thing in question is not true using the binary predicate says (instead of a ternary predicate). Formula 4 can be considered as the query. We have to express the pieces of information 5 and 6 explicitly by introducing the unary predicate true. The transformation of the formulae below into clausal form is straightforward and therefore omitted here. It consists of 11 clauses. -The symbol V. denotes exclusive or.

1. troe(isa( Q, knight))¥troe(isa( Q, knave))
2. says(P, S)---. ( true(S) +-+ troe(isa(P, knight)))

1. troe(not(C))¥troe(C)
2. troe(or(A, B))+-+ (true( A) V true( B)))

We can prove the query in many different ways. As a con­ sequence we get many trivial and hence useless answers. The (most) trivial one - a four part disjunction - can be obtained in both cases. We only need formula 1 and the query in order to infer it. But it only says that each of both persons are either knights or knaves. In case (a) (if the asked person says yes) we can get an indefinite answer consisting of only three disjuncts.

In the other case (b) there exists a definite answer. It follows a list of these possible answers where X f Y is an abbreviation of troe(isa(asked, X)) 1\ troe(isa(other, Y)) .

1. knave/ knave V knave/ knight V knight f knave V knight/ knight (trivial)
2. knave/ knave V knight/ knave V knight/ knight
3. (indefinite)
4. knave/ knight

(definite)

Before turning to our experiments we want to mention some interesting facts. Firstly, answer completeness requires that we are able to compute the indefinite and definite answer in the respective cases. Secondly, to derive these answers we need a clause set which is not minimal unsatisfiable; notice that the clauses of 1 and 4 together are (minimal) unsatisfiable yielding the trivial answer. Thirdly, 9 extension steps are needed to derive the indefinite or the definite answer respectively, while only 7 extension steps are needed to derive the trivial answer (in both cases). - These remarks indicate that it should be more difficult to find the more precise answers.

5.2 Experimental Results

We tried to get the answers from above automatically by us­ ing the theorem proving systems OTTER [McCune, 1994] which is a resolution-style theorem proving program coded in C for first order logic (with equality), SETHEO [Letz et al., 1992] which is a top-down prover for first order predi­ cate logic based on the calculus of the so-called connection tableaux which generalizes weak ME, implemented in C, and PROTEIN [Baumgartner and Furbach, 1994b] which weal­ ready introduced in Section 4. - We used the clause ordering given by the problem description, but our experiments show that the (run time) results depend on the ordering.

OTTER has some problems with computing answers be­ cause it enumerates resolvents but not all (refutational) proofs. Especially during the subsumption test, it did not take the an­ swer literals into account which are provided for computing answers. That is the reason why OTTER with (forward and backward) subsumption is not answer complete. An example which illustrates this is case (a) where the search stops after finding 15 times only the trivial answer with binary resolu­ tion. However, we find a proof by using hyper-resolution with factorization imp1ediately within 0.4s. - There is a solution to the problem with subsumption; it can be shown that we only have to take the answer literals into account during the subsumption steps. Unfortunately, it is not (yet) possible to test OTTER in this setting and find out whether this improves the behaviour, because it is not built in.

We generate answers with SETHEO by using global vari­ ables. The answers are kept in a list. By this and other tech­ nical tricks, we find the indefinite answer within l.Os and the definite answer within 0.6s. That is quite good and may be explained by the subgoal reordering heuristics built into SETHEO, which are not (yet) incorporated into our sys­ tem. But in addition, SETHEO also has subsumption con­ straints which are used in the default setting. It is not quite clear, whether these constraints destroy answer completeness in SETHEO. - Table 2 shows the timings for OTTER and SETHEO. All timings are measured on a Spare 10. The sym­ bol oo denotes the fact that no proof was found within 1 hour; that is true for OTTER applied to case (b) of our example.

PROTEIN is answer complete; that has been stated in this paper. It finds out the indefinite and definite answer for the respective case. The table in Figure 2 also shows some timings for finding these answers with PROTEIN. We tried both, plain and restart ME. In case of the restart variant we also tried its refinements: with or without ancestry restart or selection function (no contrapositives). We tried to compute the desired answers with settings where all solutions are computed in case (a) (indefinite answer). For the case (b) (definite answer) we used the setting where only definite answers are searched for. By this, we get a significant speed up of the search. - As one can see, using restart helps for this problem, since plain ME does not find the desired answers quickly, although it does so for trivial answers. But it is not quite clear which flags should be used in addition.

We investigated more puzzle examples from [Smullyan, 1978]. All our experiments corroborate the following facts: resolution has difficulties in solving puzzles because of the problem with subsumption; model elimination is better suited although it could not solve all puzzles that we tested. For ex­ ample, OTTER needs 281 .8s on puzzle #35 while PROTEIN only needs 153.1s. Further investigations are necessary. It seems that also a model generation approach is very adequate [Manthey and Bry, 1988] for these kind of problems because they often allow for finite models. Last but not least, we want to point out that both, OTTER and SETHEO do not support a procedural reading of program clauses -they need all contra­ positives- but PROTEIN does; and that is useful if we want to use logic as a real programming language.

6 Conclusion

To conclude, it seems to be very promising to use ME as a base calculus for computing answers in disjunctive logic programming. In this paper, we introduce (among others) the ancestry restart variant which is quite well suited for this purpose. We also give some practical evidence. Nevertheless, further investigation is necessary in order to find out yet more efficient calculi and to incorporate nonmonotonic extensions.

Acknowledgements

We would like to thank Fran¥ois Bry, Jiirgen Dix, Bertram FronhOfer, Reinhold Letz and William W. McCune for helpful discussions, and Olaf Menkens and Dorothea Schafer for their implementational work.