On the Solution of Schubert's Steamroller in Many-Sorted Logic

1. lntroducüon

In 1978 Schubert set up the following challenge problem:

Wolves, foxes, birds, caterpillars, and snails are animals, and there are some of each of them. Also there are some grains, and grains are plants. Every animal eilher likes to eat all plants or all animals much smaller than itself that like to eat some plants. Caterpillars and snails are much smaller than birds, which are much smaller than foxes, which in turn are much smaller than wolves. Wolves do not like to eat foxes or grains, while birds like to eat caterpillars but not snails . Caterpillars and snails like to eat some plants. Therefore there is an animal that likes to eat a grain-eating animal.

An axiomatisation of this problern as given in [13] is as follows:

1. 3w.f ,b ,C ,S ,g (W(w)AF(/)AB(b )AC(c )AS(s )AG(g ))
2. V'z ((W(z )vF(z )vB(z )vC(z )vS(z ))-+A(z))
3. V'z (G(z )-+P(z ))
4. V'z(A(z)-+ (V'y(P(y)-+E(z ,y))v V'y ((A(y)AM(y,z )A3 z (P(z)AE(y ,z ))}-+E(z ,y ))))
5. V'z ,y(((C(z )vS(z ))AB(y ))-+M(x ,y ))
6. (Bu) V'x ,y((B(x )AF(y))-+M(x ,y))
7. (?u) V'x ,y((F(z )AW(y))-+M(x ,y))
8. (Bu) V'z ,y (((F(x )vG(x ))AW(y))-> ~E(y ,X))
9. V'z ,y ((B(x )AC(y ))-+E(x ,y ))
10. V'z ,y ((B(x )AS(y ))-+ ~E(x ,y ))
11. V'x ((C(x )vS(z ))-+3y (P(y )AE(z ,y)))

(12u)

3z ,y(A(z )AA(y)AV'z(G(z)-+(E(z ,y)AE(y ,z))))

· This work was partially funded by the SERC under grant GR/C/65148.

On the Solution of Schubert 's Steamroller in :Many Sorted Logic.

Anthony G Cohn

Department of Computer Science University of Warwiek Coventry CV4 ?AL UK

The clausal form contains 27 clauses with 6::> literals and until very recently no computer generated refutation had been generatedn even though a hand built proof has been found: the search space is extremely large; there are 94 potential initial resolvents and 8 potential factors and the hand computed solution requires 33 inference steps. The clausal form of the above axiomatisation is given below.

(1cu) to (Bcu) come from (1u) . (?cu) through to (12cu) come from (2u) and (3u). (13cu) comes from ( 4 u) (14cu) through to (17cu) come from (5u), (6u) and (?u): (18cu), (19cu) and (21cu) come from (Bu) and (lOu). (20cu) comes from (9u) . (22cu) through (25cu) are the skolemised clauses derived from (11 u). Stmllarly (26cu) 8 .1 (27cu) come from the negation of (12u) .

n These solutions will be described in the last section.

Recently, Walther, [13] has derived a computer solution to the problern by reaxiomatising it in a many sorted logic before giving it to the MKRP-system at Karlsruhe [12] . His many sorted formulation has a significantly reduced search space: only 12 clauses with 16 literals with an initial search space of 12 posslbie inferences and a total of 10 new clauses in the deduced proof .

The purpese of this paper is to show that further efficiency is possible by recasting the problern in a different many sorted logic [3, 4] which possesses a number of additional features which increase its expressiveness as compared to Walther's logic [ 12] and the other many sorted logics to be found in the literature, eg [6, 6, 2, 5] . A table comparing the formulation of the problern in the different logics may be found towards the end of this paper in figure 2.

2. Willther's Axiomatisation

For convenience, Walther's many sorted axiomatisation is repeated here in order to better compare the formulations in the two different many sorted logics.

In his logic type declarations define the sort of function and constant symbols (his predicate symbols may also be typed but this feature is not needed in this example) . Sort declarations define the sort hierarchy. Animals, plants, grains, wolves , foxes, birds, caterpillars and snails are all sorts, named A, P, G, W, F, B, C and S respectively.

(27w) ! ~E(a1,a2), ~E(a2,j(a1 , 112))j

The symbols 111 , /1 etc are all typed variables with the sort of the corresponding upper case Ietter. (1w) to (6w) define a signature and play no part in the proof.

As already mentioned, Walther's proof is 10 steps lang (9 resolutions and a factorisation) . It is reproduced below (in a slightly altered form to show the factorisation explicitly).

(26w) !E(a1,p1), ~M(a2,a1), ~E(a2,p2), ~ E(a2,j(a1,112))j 13w(4)+27w( l ) (29w) !E(a1,p1), ~M(a2, 111) , ~E(a2,j(a1 ,a2))j factor of 26w (30w) !E(w1 ,p1), ~ E(/1 ,j(w1 j1))j 17w(1)+29w(2) (31 w) ! ~E(/1,j(w1 j1))j 19w(1)+30w(1) (32w) !E(!1,p1), ~E(b 1,j(/1 ,b1))j 16w(1)+29w(2) (33w)! ~ E(b1,j(/1,b1))j 31 w(1)+32w(1) (34w) !E(b2,p1) , ~M(s 1,b2), ~E(s1,p2)j 13w(4)+21 w(1) (35w) ! ~ M(s1,b2) , ~ E(s1,p2)l 33w(1)+34w(l) (36w)! ~E(s1,p2)j 15w(1)+35w(1) (37w) !l 25w(1)+36w( 1)

He attributes the success of his system in finding a proof to the significant reduction in the clause set and to the restriction on unification preventing the matehing of variables with incompatible sorts . For example clauses (20w) and (21 w) have no resolvent because c 1 and s 1 cannot be unified. In the unsorted case the two clauses (20cu) and (21cu) do resolve to yield! ~B(x) , ~ C(y), ~S(y)l . This can then be resolved with (3cu) to yield ! ~C(y) , ~ S(y)j . However further inference will now yield a pure clause: eilher ! ~ S(c)j or ! ~ C(s)l , where c and s are skolem constants . The dead end is detected much earlier in the many sorted logic .

3. ABrief Description of LI..AioiA···

The many sorted logic LLAMA [ 4, 3] is unusual in that the quantifiers are unsorted; the restriction on the range of a quantified variable derives from the argument positions of the function and predicat e symbols that it occupies; associated with every non­ logical symbol cx is a sorti:ng function ä of the same arity which describes how its sort varies with the sorts of its inputs; polymorphic functions and predicates are thus easily expressible and statements usually requiring several assertions may be compactly expressed by a single assertion. The sort structure itself is a complete boolean lattice . The top (T) element is interpreted as the universe of discourse and the bottarn ( ..L) is interpreted as the empty set. Expressions of sort ..L do not denote anything and are thus nonsense; they are said to be ülsorted. . Sorts may be referred to eilher directly or with an expression containing least upper bound (U), greatest lower bound (n) or relative complement (\) operators.

··· Logic Lacking A lleaningful Acronym. Having sought a suitable name for the logic for a lang time, I am indebted to Graeme Ritchie for this suggestion.

Furthermore, by specifying the result sort of predicates to be one of four special boolean sorts TT, FF, UU, EE (representing 'true', 'false', 'either true or false', and 'nonsense'), it is sometimes possible to detect that a formula is Contradietory or tautologous without resort to general inference rules . Expressiveness can be further improved by allowing the sort of a term to be a more general sort than the sort of the argument position it occupies. However this feature is not needed for the current problem.

Associated with every formula in the logic is a Sort Array (SA} which is a mapping from sort environments to boolean sorts . A sort environment is a mapping from variables to sorts. Thus a SA records what the sort of a formula is, depending on what sorts its constituent variables are regarded as taking . A good way to view a SA is as an n dimensional array where n is the number of variables in the formula. Each dimension is indexed by the different sorts and each position in the array will contain one of the four boolean sorts FF. TT, UU or EE. If all entries are EE then the formula is nonsense (or illsorted) and can be deleted. Entries which are TT will be ignored by the system (effectively treated as though they were EE) since they cannot lead to a refutation. In the case of a clausal logic, if any of the entries are FF then the formula is a contradiction since all variables are universally quantified.

Inference in the logic includes ordinary resolution but there are some new inference rules. In particular it is sometimes possible to evaluate literals because they are always of sort FF in the possible environments of the SA of the clause . Evaluated literals may be deleted without having to resolve them away. It is sometimes advantageaus to restriet the SA of a clause (ie restriet the set of possible sort environments in the SA, by changing some of the entries in the SA to EE) in order to evaluate a literal. Examples of such inferences will be found later on in the paper.

4. An Axiomatisation in LI..A1lA.

We use all the sorts of Walther's axiomatisation and some additional ones. As will be discussed later, the sort CUS allows the axiomatisation tobe one clause smaller than it would otherwise be, and the sort P\G is added because, since Gis a strict subsort···· of P, there must

···· Actually it does not follow that G is a strict subsort of P it the sort structure is derived from the unsorted axiomatisation, although it could be argued that the original English statement of the problern does implicitly imply this is in fact so . Walther's axiomatisation also specifies G to be a strict subsort of P . In any case this detail is not crucial to the problem.

It should also be noted that in LLAMA the sorts B, F, C, S, W, G, and P\G are all disjoint : their interpretations are non-overlapping sets (this is because, as currently formulated, LLAMA requires complete knowledge about the sort structure). Again, this disjointness is not present in the unsorted axiomatisation nor is it present in Walther's formulation, nor is it stated explicitly in the English statement of the problem, although it is true in the real world. However, this disjointness information is only used to reduce the search space and will not be used in the proof itself since there are no positive sort literals . It may be noted that Stickel's solution of the steamroller which is discussed later also assumes the disjointness of these sorts.

be a sort which is interpreted as all those plants which are not grains. The use of P\G will also be discussed later. Part of the hierarchy is depicted in figure 1.

Although LLAMA actually requires the sort lattice tobe a complete boolean lattice with (in this case) z7 sorts, for simplicity only those needed to dehne the sorting functions for the non logical symbols are shown. Six further sorts (A\W, A\W\B, A\W\F, A\ B, A\C and A\W\S) are used during the proof (see clauses 1 and 3 below) .

The sorting functions for the various non-logical symbols (including skolem constants) are as follows. Entries not given are assumed to be EE (ie undefined) unless otherwise inferable .

The sorting function for a characteristic (or sort) predicate T is

Eg, the sorting function for the predicate Pis:

Note how the sorting functions for both M and E make use of LLAMA's polymorphism to encode much of the information about M and E. This type of polymorphism has been called adhoc polymorphism by Strachey [11] (or overloading) and should be distinguished from the parametric polymorphism to be found in, for example, (9].

The clausal form of the axioms comes out as just the following three clauses. The sort environments for which the corresponding SA is not EE or TT are listed next to each clause (the first column gives the result sort). Environments for which a clause is TT can be ignored during a refutation because the clause is tautologous in these environments and thus they can be deleted for the same reason as ordinary tautologous clauses can. These SAs are not input with the axioms but are derived using the sorting functions by an algorithm to be found in [ 4] .

• (1)! ,p(pJ), ,p(pz),E(al,pl), ,M(a2,a1), , E(a2,p2),E(aJ,a2)l

(2) !E(csJ,h(csJ))l

1. ! ,E(a1 ,a2), ,E(a2,j(a1 ,az))l

These axioms are derived· from the unsorted axioms 4u, 11u and the negation of 12u respectively. All the other unsorted axioms have been subsumed by the sort lattice and the sorting functions .

Thus this axiomatisation has just 3 clauses and 9 literals! There are only 4 possible resolvents initially. There are also some other possible inferences initially because certain literals are evaluable. In particular literals 1(1), 1(2), 1(4) can only be evaluated since there are no positive occurrences of P or M. (In fact characteristic literals such as P(p1) may always be evaluated immediately without losing completeness). Thus 1 could be preprocessed to:

( 1 ') !E(al,pl), ,E(a2,p2),E(al ,az)l

Thus there are now only 6 literals overall. There are four possible resolvents and three possible evaluations (on 1'(1), 1'(3), and 3(1)) in this modified input clause set . None of the three clauses can be factored.

· It should be quite possible to derive this axiomatisation (including the sorting functions) automatically from Walther's formulation or perhaps even from the unsorted formulation.

A proof .. goes like this.

(4) !E(a1,p1), -E(a2,p2), -E(a2,j(a1 ,az))l 1 '(3)+3( 1)

(5) !E(al,pl), ,E(az,j(aJ,a2))l factor of 4

(6) !E(a3,pl), -E(a2,p2),E(aJ,a2)l 5(2)+1 '(1)

Since Iitera! 6(3) is always false in the environments of clause 6 it can be evaluated and deleted from the clause without changing the SA or the meaning of the clause to produce a simpler clause 6':

(6') !E(a3,pl), ,E(a2,p2)l

(8) !E(al,pl),E(aJ,a2)l 7(1 )+ 1 '(2)

We have now derived a clause with an environment for which it is FF ie false. Since variables are universally quantified such a clause is a contradiction and we have our desired refutation. In an ordinary clausal logic, only a null clause indicates a falsehood but in this calculus it is possible for a non null clause to be contradictory by virtue of sortal information.

Note that this proof is linear; neither the unsorted hand produced proof of Schubert nor the rnany sorted proof of Wallher are linear. Linearising a non-linear proof orten increases its length. The total number number of inference steps (not counting preprocessing and simplifications) is only 5 steps. This compares with 10 steps in [14] . The inclusion of the extra sort CUS

·· This proof is hand produced. However, an implementation of the logic will be finished in the near future .

saves one unit clause in the axioroatisation of the problero; this reduces the search space slightly (the MKRP systero could also take advantage of this) bul does not reduce the proof length since (23w) is not used in the proof.

Part of the saving coroes froro the ability to represent inforroation such as "caterpillars are rouch sroaller than birds" not as unit clauses as Watther has to (14w) but as sorting functions . Because this inforroation can be representcd without using a clause a reduction in the search space occurs . The sorting functions for M and E are then used to advantage during the proof process to evaluate certain literals . Evaluations which can be perforroed without havin~ to restriet the SA are entirely 'free'. (They are called elementary evaluations in [ 4] ). They do not increase the search space because the old clause can be deleted. An example is the evaluation performed in producing clause 6'. Also, it has already been argued that it is beneficial to evaluate pure (ie not resolvable) literals as soon as possible, as was done in producing clause 1 '. However even a non elementary evaluation may not actually increase the search space since the parent clause may be restricted to exclude the sort environroent used to produce the evaluation without losing coropleteness . No non eleroentary evaluations were perfo.rmed in the proof above though they might be used in a different branch of the search space (for exarople we have already noted above that three non elementary evaluations are possible initially (1 '1 ), 1 '(3) and 3(1)) .

Obviously the overhead of computing and maintaining the SAs for the clauses has to be taken into consideration but this should be overshadowed by the reduction of the search space which accrues through use of the many sorted logic in roost cases: the cost of the SA operations appears to be some polynomia!··· of the nurober of sorts and the nurober of variables in a clause, whilst the size of the search space is in generat exponential in the nurober of clauses . The occasions when savings are unlikely to be realised are when there is little sortal structure in the problero. In this case the SAs will be very !arge (ie will be UU in roost environments), few evaluations will be possible and inference will be no better than in an unsorted logic with the additional burden of having to roaintain the SAs .

A second reason why the LLAMA proof is shorter is because of its polymorphism. Inspection of Walther's proof (or indeed of the unsorted proof) shows that a Iitera! with predicate syrobol M is resolved away three times during the proof (in producing clauses 30w, 32w and 36w) . Each time a different unit clause is involved. These steps are all corobined in the evaluation of the polyroorphic clause ( 1) to produce clause ( 1 '). The important pointisthat (1') is still polymorphic···· . The Iitera! involving M has been deleted but without having to make such a comroitment as to the precise sorts of the variables as in a non-polymorphic logic . In a non­ polyroorphic many sorted logic once that Iitera! has been resolved away then a coromitment is roade as to which precise sorts the variables involved in the resolution should be. For exarople, (30w) is a result of a resolution involving M. But now aJ and a2 have been irrevocably chosen to be of sort Wand F respeclively.

··· AnalySing the complexity of the SA operations is an area for further research.

···· Note that .l' would have to be represented as three clauses in Walther's logic, each one corresponding to one of the sort environments of 1 '. Thus polymorphisro can allow one to obtain some "non clausal" effects.

The point is of course that instead of choosing to resolve (29w) agairrst (17w) an inference engirre roight just as weil have chosen any of the other three unit clauses involving M, for exarople (14w). In this case aJ and a2 would now be of sort B and C respectively. However this resolution cannot Iead to a refutation (which is why the environroent <B,C,P ,P> does not appear in the SA for (1'): it is tautologous and thus wtll not be used in a refutation) . Thus any further inference involving this resolvent would be totally wasted. The advantage of a polyroorphic logic thus is that generality is retained and choices involving the precise sorts of variables can be delayed. This arguroent would hold even if M had been resolved away conventionally rather than by evaluation. It would also hold even if the environment <B,C,P,P> were still in the SA for ( 1 ') because in the LLAMA proof the decision about the sorts of aJ and a2 is made as needed when resolving to produce clauses 4, 6 and B.

Thus adding polyroorphisro to a many sorted logic in this way does seem to add genuine extra power. One could imagine that a logic such as Walther's could perhaps be siroulated with an unsorted logic by running the sort axioros intelligently (eg never resolving on an uninstantiated characteristic Iitera!, but choosing instantiated characteristic literals as top priority when available and also checking characteristic literals in the same clause for inconsistency by testing whether the clause is subsuroed by any sort lattice axioro) but it is not obvious how LLAMA could be directly siroulated in such a manner with a clausal unsorted logic.

5. Final Remarks

Soroe of the statistics appertaining to the three axioroatisations of the Steamroller are suroroarised in the table of figure 2.

This exarople deroonstrates the advantage not only of using a roany sorted logic, but also the value of polyroorphism· and of using the four boolean sorts for describing the sortal behaviour of predicates.

Schubert's Stearoroller has also recently been solved by two other autoroated reasoning systeros; in both cases special purpose reasoning systems were employed. The ITP system [7] has a system of "qualifier" literals which can be used to simulate a many sorted logic to a limited extent. The success of the ITP system on the Steamroller problern is reported in [10] but no details of the proof were given so no detailed comparison is possible. Stickel has also solved the steamroller with his non clausal logic which "builds in theories". 1heory resolution removes the need to resolve upon axioms in the theory by utilising a decision procedure that can determine the unsatistiability of a set of clauses using predicates in the theory. The statistics in the table of tigure 3 show the results of Stickel's system for (a) no knowledge built in (b) 2u-3u built in (c) 2u-3u and 5u-llu built in··.

· Note that the iroplicit restriction on the quantification on variables froro the arguroents places they occur in is essential to exploiting LLAMA's polyroorphism since variables with unique sorts exclude the possibility of polymorphic clauses such as 1 '.

These figures are taken directly from [10] . No statistics on the original size of the search space were given. The times refer to a system running on a Symbolics 3600. These results show a dramatic improvement in the size of the search space by building in axioms. A solution is found about 100 times faster with (c) compared to (a)! Thus although a proof can be found with no special purpose inference machinery for handling taxonomic information it is very expensive to compute···. However the proof length is stilllonger that in eilher of the many sorted solutions. Theory resolution can handle characteristic literals more efficiently than a standard unsorted logic but cannot eliminate them altogether as is possible in many sorted logic. However theory resolution is more general than a many sorted logic : for example paramodulation can be viewed as an instance ot theory resolution.

In this problem, sorts have managed to reduce the amount of normal inference required to almost nothing, but of course in !arger problems there will still be a non trivial amount of such inference required, for it is not claimed that a many sorted logic is a generat panacea. However it does seem to be a useful weapon in attacking large search spaces.

6. Ack:nowledgements

My special thanks go to Christoph Wallher for his helpful comments on a drart of this paper. I have also had useful discussions with Alan Frisch, Pat Hayes and Bob Kowlalski.

·· For comparison, LLAMA "builds in" 1u-3u and 5u-10u while Walther's many sorted formulation "builds ln" 1u3u.

··· Stickel also reports a personal communication from Watther that the MKRP system found an unsorted solutior: too. However this took about 10 times Ionger than w1th the sorted formulation of the problern and relied heavily on the TERMINATOR module [1] (a fast procedure for finding unit refutations) .

7. Heferences

1. G Antoniou and H J Ohlback, "TERMINATOR," in Proc JJCAJ8, Karlsruhe ( 1983).
2. D de Champeaux, "A Theorem Prover Dating a Semantic Network," in Proc AJSBIGJ Conf an AI, Harnburg (1978).
3. A G Cohn, "Improving the Expressivenass of Many Sorted Logic," in Proc AAAJ, Washington DC (1983) .
4. [ 4] A G Cohn, "Mechanising a Particularly .Expressive Many Sorted Logic," PhD Thesis, University of Essex (1983) .
5. H B Enderton, A Mathematical Jntrod.uction to Logic, Academic Press (1972).
6. L J Henschen, "N-Sorted Logic for Automatie Theorem Proving in Higher Order Logic," in Proc. ACM Conference, Boston (1972).
7. E Lusk and R A Overbeek, "The Automated Reasoning System ITP," Technical Report ANL 84 27, Argonne National Laboratory (1984).
8. J R McSkimin and J Minker, "The Use of a Semantic Network in a Deductive Question Answering System," in Proc JJCAJ5, Garnbridge (1977) .
9. A Mycroft and R A O'Keefe, "A Polymorphie Type System for Prolog," Artifi.cial JnteUigence 23( 1984) .
10. M E Stickel. "Automated Deduction by Theory Resolution," Dratt Report, SRI International (1984) .
11. C Strachey, "Fundamental Concepts in Programming Languages," Vnpublished. notes for a NATOSummerSchool, (1967). ·
12. C Walther, "A Many Sorted Calculus Based on Resolution and Paramodulation," in JJCAI 8, Karlsruhe (1983).
13. C Walther, Schubert's Steamroller- A Case Stud.ym Many Sorted. Resolution, Universitat Karlsruhe (1984).
14. C Walther, "A Mechanical Solution of Schubert's Steamroller by Many Sorted Resolution," in Proc AAAI. Austin, Texas ( 1984).