Extending the Resolution Method with Sorts

1 Introduction

One promising approach for increasing the strength of a_ut~mated reasoning systems is the integration of theo­ nes mto the standard first-order resolution calculus. For special theories there are more efficient methods than standard resolution. One theory that has been investi­ gated is the theory of unary predicates called "sorts" see e.g. the logics of Beierle et al. [Beierle et al., 1992], Cohn [Cohn, 1992], Frisch [Frisch, 1991], Schmidt-SchauB [Sc~midt-SchauB, 1989], Walther [Walther, 1987], or Weidenbach et al. [Weidenbach and Ohlbach, 1990]. All these approaches offer special language constructs and reasoning facilities for sorts. They differ in the restric­ tions imposed on the sort theory and the way the sort theory is processed. This will be discussed in more detail in Section 4. In the following I will explain why the ap­ proach presented in this paper generalizes and improves existing results. What all approaches have in common is the incorporation of sorted reasoning in the unification algorithm. Here is an example for sorted resolution in comparison with standard resolution.

*This work was supported by the ESPRIT project 6471 MEDLAR of the European Community

The database d consisting of the clauses

d:

1. Man(peter)
2. Man(x) =? Human(x)
3. Human(y) =? Human(father(y))
4. Human(y) 1\ Human(z) =? Love(y, z)

can be represented in a sorted formalization by the database d' of clauses:

d':

1. Man(peter)
2. Human( X Man)
3. Human(father(yHuman))
4. ( 4) Love(YHuman1 ZHuman)

An immediate difference between d and d' is that d' contains fewer literals. The negative sort literals (2)1 , {3)1, (4)1 and (4)2 of dare replaced by restrictions on the variables. (In order to refer to clauses and literals the clause number and the position of the literal in the clause are used. Thus ( 4)1 refers to the literal Human(y) of clause (4).) Second, there are infinitely many non re­ ~undant resolv~nts derivable from d (e.g. clause (3) with Itself) whereas m d' no resolution step is possible at all. In order to derive the query Love(peter,father(peter)) from d and d' the clause

1. -,Love(peter,father(peter))

is added to the databases. Using d four resolution steps and one factorization step are needed, whereas using d', one single resolution step between (5)1 and ( 4)1 yields the empty clause. Sorted unification checks whether the terms peter and father(peter) are of sort Human. This can be done by exploiting the sort theory consisting of th~ positive sort literals (1)1, (2)1, and (3)1 of d'. Thus thnd, the sorted approach succeeds with fewer inference steps. This sim~le example demonstrates the advantages of sorted reasonmg compared to standard resolution.

In general, the sorted unification algorithm is more complex than standard unification. As compared to standard resolution this has to be taken into account. For nearly all examples the behaviour of sorted uni­ fication is not harmful. In particular, for sort theo­ ries that are difficult the sorted unification process is much more efficient than standard resolution. This will be explained in Section 4. For !:::..' the complexity of sorted unification is the same as for standard unifica­ tion. !:::..' is a simple database. It can be processed (after translation in the respective formalism) in the described way by all approaches mentioned above [Beierle et al., 1992; Cohn, 1992; Frisch, 1991; Schmidt-Schaufi, 1989; Walther, 1987; Weidenbach and Ohlbach, 1990]. For the next database !:::.." this is not the case. The unary predi­ cates Man and Woman cannot be represented as a sort in the logics of Frisch, Schmidt-Schaufi, and Walther. They can be represented in the logics of Beierle et al., Cohn, and Weidenbach, but their calculi consist of more rules other than the usual resolution and factorization rule. In this paper I will show how any unary predicate can be processed as a sort just by modifying the standard resolution method. Now consider!:::..":

From!:::.." the query Love(peter, mary) must be derivable. Adding the clause (5) -,Love(peter, mary) to !:::.." offers only two resolution possibilities between (4)1 and (3)1 and between (5)1 and (2)1. For the two resolution steps sorted unification has to guarantee that peter is of sort Woman or peter is of sort Man, respectively. Clause (1) is valid if peter is of sort Man or peter is of sort Woman. Therefore at least one declaration of clause (1) has to be considered for sorted unification. For!:::..', the sort theory consists of sort literals occurring in unit clauses. Now it becomes obvious that considering such sort theories is too restrictive to get a complete calculus. From every clause consisting of positive sort literals ex­ actly one literal must be chosen for the sort theory (see also Theorem 8). For!:::.." if we choose (1)1, Man(peter) as the sort theory, from (5)1 and (2)1 we derive by reso­ lution (6) Woman(peter). The literal Woman(peter) is the result of sorted unification, because (1)1 is not the only literal of clause (1). Clause (6) subsumes clause (1). The sort theory must be changed to the sort literal (6)1, Woman(peter). Then the empty clause is derived from (4)1 and (3)1.

The example demonstrates three important aspects of the resolution method extended with sorts:

• A notion of "conditional well sortedness" is needed, where the additional literals of declarations com­ ing from non-unit clauses are collected. (See Sec­ tion 2.2.)
• The declarations considered by sorted unification have to be changed dynamically during the deduc­ tion process. (See Theorem 8.)
• From each clause which consists of declarations only, at least one declaration must be chosen for sorted

unification in order to obtain a complete calculus. (See Theorem 8.)

The next section introduces the new sorted resolu­ tion method. The method is applied to two examples in Section 3. Section 4 relates the new sorted resolu­ tion method to existing work in a more abstract way. The paper ends with a short summary in Section 5. All proofs are omitted and can be found in an internal report lWeidenbach, 1991].

2 The Sorted Resolution Method

The starting point of the new method is the standard resolution method for first-order logic. First, the stan­ dard syntax is extended with sorts. Then the notion of well sortedness is introduced. Finally, the modified res­ olution and factorization rule and the sorted unification procedure are presented.

2.1 Syntax and Semantics

Syntax: The standard signature E consisting of the sets V:E, P:E, FE of variables, predicates, and functions respec­ tively, is extended in the following way. Unary predicates are called sorts. S:E is the set of all sorts (SE ~ PE)· The functionS, S: VE-+ SE U {T}, where T rt E, maps vari­ ables to sorts such that for each sort S E SE U {T} there are infinitely many variables x with S(x) = S. In ex­ amples (as in !:::..', !:::..") it is indicated that a variable x has sort S by writing xs. If not stated otherwise, vari­ ables not annotated with a sort have sort T. Terms, literals, clauses, formulae and substitutions are defined in the usual (unsorted) way. Literals built from sorts are called sort literals. Positive sort literals are called declarations.

With DOM(u): = {x I xu =/; x} we denote the finite domain of a substitution u. Specific substitutions are described by their variable-term pairs, e.g. { x ~--+ a} de­ notes the substitution x maps to a.

The function V maps terms, formulae and sets of such expressions to their variables.

Semantics: The semantics of sorted variables is given by the two relativization rules

where S(x) = S, S =/; T, S(y) =Tandy does not occur in the formula :F. Variables of sort T (the top sort) have the same semantics as standard variables. If the first relativization rule is applied to !:::..', !:::.. is obtained. The database !:::.. is special case of a sorted database where all variables have sort T.

2.2 Conditional Well Sorted Expressions

The processing of !:::.." showed the need for an extended notion of well-sortedness. A conditional well sorted ex­ pression consists of a well sorted expression in the usual sense [Schmidt-Schau6, 1989; Frisch, 1991] plus a set of literals. Conditional expressions are written with a prime.

Definition 1 (Conditional Expressions)

A pair (L , C) is called a conditional declaration (con­ ditional term, conditional substitution) if C is a finite set of literals and L a declaration (term, substitution).

The next step is to define what we mean by a sort theory. A sort theory C is a set of conditional declara­ tions. The notion of well-sorted terms and sorted unifi­ cation is defined with respect to a sort theory C. The sort theory is always a part of the database (signature), although it is separated away and static in nearly all approaches known so far [Stickel, 1985; Walther, 1987; Schmidt-SchauB, 1989; Biirckert, 1991; Frisch, 1991; Beierle et al. , 1992; Cohn, 1992]. In this approach the sort theory is chosen dynamically from the database. In the course of generating new clauses it may happen that the sort theory changes {see .6."). Nevertheless we can assume that C is always finite and all conditional dec­ larations are variable disjoint. The following definitions are presented with respect to a fixed sort theory C.

Definition 2 (Conditional Well Sorted Terms)

The set of conditional well sorted terms (abbreviated by cws. terms) Ts of sort Sis recursively defined by:

• for every variable x E Vr:, (x , 0) E Ts(z)
• for every conditional declaration (S(t) , C) E C, {t , C) E Ts
• for every conditional well sorted term (t, C) E Ts (S =/= T), substitution u:= {x1~-+ t1, . .. ,Xn ~--+ tn}, with (t;, C;) E Ts(z;) for all i, (U; C;) ~ D for some finite set of literals D, (tu, Cu U D) E Ts
• for every term t we have {t, 0) E TT

We define TJ:= {(t,0) I {t , 0) E Ts}. The relation!;;;; denotes the subsort relationship. If S and T are sorts, then we define S C T iff there exists a variable x with S( x) = S and x E TT. A sort S is called empty if Ts does not contain a ground term. A conditional substi­ tution u' = ( u, C) is called conditional well sorted if for every x; E DOM(u), (x;u, C;) E Ts(z;) for some C; and (U; C;) ~ C. The composition of two cws. substitu­ tions can be computed by r'u':= (ru,KuUC), where u' = ( u, C), r' = ( T, K). The result of the composition is again a cws. substitution. Thus the set of all cws. substitutions forms a monoid.

The relation !;;;; and the test whether a sort is empty can be decided in linear time with respect to the number of declarations in C. The question whether a term t is included in Ts for some sort S is decidable in at most O(n 2 * m) time where m = ILl and n is the number of symbols in t [Weidenbach, 1993]. This is important because these relations are frequently needed in sorted unification and for the application of the resolution rule.

Example: Applying Definition 2 to .6.' with C = {{1)1, {2)1, {3)1}, TMan = {(peter, 0), {x1, 0), {x2, 0), ... } where S(x;) = Man and THuman= TMan U {(father;(peter),0), {father;(Y;),0), (Yl,0), (y2,0), . . . } where S(y;) = Human and Man !;;;; Human, Man !;;;; T, Human!;;;; T.

Applying Definition 2 to .6." with C = {(1)1}, TMan = {(x1 , 0), {x2,0), ... , (peter,{Woman(peter)})}

with S(x;) = Man . Twoman = {(y;,0)} with S(y, ) = Woman. The sort Woman is empty. If we choose C = {(1)2} the sort Man would be empty and Twoman contains the term (peter, { M an(peter)}) . For a complete resolution calculus it suffices to choose exactly one of the literals (1)1 or {1)2.

The algorithm COMP compiles negative sort into vari­ able restrictions. This is done with respect to the sort theory C consisting of all declarations which occur in a unit clause. COMP is a generalization of the sort gener­ ating algorithm SOGEN suggested by Schmidt-SchauB [Schmidt-SchauB, 1989] .

Algorithm 3 (COMP) The input of the algorithm is a database of clauses A.

1. Select all declarations occurring in unit clauses for c.
2. For every clause C = -,T(x) V C':
3. (a) if S(x) !;;;; T and S(x) is not empty or x E V(C'), delete -,T(x)
4. (b) if T !;;;; S(x) and x E V(C') replace C by C'{x ~--+ YT}
5. (c) if a new unit clause containing a declaration is derived, add the declaration to C.

COMP is an efficient alg~rithm in at most 0( m 2 ) time where m = IAI for some database A.

Example: Applying COMP to .6. results in .6.'. The only declaration occurring in a unit clause is Man(peter), whence C = {(1)1} (Step 1 of COMP). By Definition 2 the sort Man is not empty and Human is empty. Step 2 of the algorithm is now applicable to {2)1 because Man !;;;; T . A new unit clause is derived and the declaration Human(xMan) is added to C. Now the sort Human is not empty and Step 2 is applicable to (3)1, {4)1, and ( 4) 2 of .6. resulting in .6.'.

2.3 Sorted Resolution

For the definition of the sorted unification procedure GSOUP (General Sorted Unification Procedure) the standard notions of unification theory (see [Siekmann, 1989]) are used. The input of the unification procedure is a unification problem f = { S1 = t1, .. . , Sn = tn} . r is called solved if it has the form r = {xl = tl , . .. , Xn = tn}, where x; =/= Xj for i =/= j, x; f/. V(t;) for all i and j, and t; E Ts(z;) for all i.

Definition 4 (GSOUP) The following five sorted rules (see Table 1) and the six standard rules Tautol­ ogy, Decomposition, Application, Orientation, Clash , and Cycle (e.g. see [Siekmann, 1989]) are applied to the unification problem r until it is solved or the problem is found to be unsolvable.

In order to compute a cws. substitution from a solved unification problem, we have to do the following. Let f = { Xl = t1, ... , Xn = tn} be the solved unification problem, then u: = { x1 ~--+ t1, . .. , Xn ~--+ tn} is the corre­ sponding unifier. u': = (u, C) is a cws. mgu if we have (t;, C;) E Ts(z;) for all i and C = U; C;. From a solved unification problem it may be possible to compute sev­ eral (but only finitely many) cws. mgu's.

Lemma 5 (GSOUP is Sound and Complete) Ifu' is a conditional substitution computed by the procedure, then u' solves r and u' is conditional well sorted. If r' is a cws. ground substitution solving r, then there is a cws. substitution u' computed by the unification proce­ dure and a cws. substitution .A', such that u' .A' = r' with respect to V(r). If in the rule Sorted Fail, the condition concerning empty sorts is erased, the unification proce­ dure is complete with respect to all cws. substitutions.

Lemma 6 Sorted unification is undecidable and of uni­ fication type infinitary.

Lemma 6 is a worst case result. For restricted sort theories better results are known (see [Schmidt-SchauB, 1989; Uribe, 1992; Cohn, 1992; Weidenbach, 1993]). GSOUP can be implemented in a way such that it has the appropriate complexity properties for restricted sort theories.

For the resolution rule it is necessary to keep track of the sorts S; occurring with the variables of the parent clauses but not with the variables of the re­ solvent. Every disappearing S; must be non-empty and the corresponding conditions have to be added to the resolvent . For example, building a resolvent be­ tween -.Love(ZMan, mary) and Love(ZMan, mary) by us­ ing .C = {(Man(peter), { Woman(peter)})} results in the clause Woman(peter). Note that the unification prob­ lem r = {X Man = ZMan} is solved, (zMan, 0) E TMan, and the only cws. unifier is ({zMan ~ ZMan},0) .

Definition 7 (Resolution and Factorization) The rules are

where u' = (u, D) is a cws. mgu of P(tt , ... , tn) and P( s1, ... , Sn) and E is a set of literals (conditions) which guarantees the sorts attached to variables occurring in the codomain of u but not in C1 u V C2u V D to be non­ empty.

The soundness of the rules follows immediately from their form and the soundness of the unification algorithm [Weidenbach, 1991]. The set E of non-emptiness con­ ditions can be computed using Definition 2 for ground terms . .

Theorem 8 (Completeness Theorem) Let A be a clause database. We choose .C: = {(S;(t;), {Li,l. ... , L;,n,)} such that for each clause C; E A only contain­ ing declarations we choose exactly one declaration S;(t;) with C; = S;(t;) V L;,t V ... V L;,n; ·

If A is unsatisfiable there exists a derivation of the empty clause using resolution and factorization. The set .C must be updated every time a new declaration clause is derived.

3 Applications

The first application is a puzzle called "The Lion and the Unicorn" which can be found in one of Smullyan's books [Smullyan, 1978] and was previously discussed by Ohlbach, Schmidt-SchauB, and Weidenbach [Ohlbach and Schmidt-Schauss, 1985; Weidenbach and Ohlbach, 1990]. The lion and the unicorn are strange creatures which lie on certain days of the week and tell the truth on the other days. The lion lies on Mondays, Tuesdays and Wednesdays and the unicorn lies on Thursdays, Fri­ days and Saturdays. In order to solve the puzzle it must be figured out what day we have if they both make the statement "yesterday was one of my lying days" .

In standard first-order logic the example is expressed by 47 clauses with 109 literals. After the application of COMP 47 clauses with 55 literals are left. The example is complicated because it contains recursive clauses and sort literals occur together with three place literals.The query is

which states that there is a day x when both the lion and the unicorn say that yesterday was one of the days they lie. The query can be further complicated by increasing the nesting depth of the function f (for "yesterday") .

Using existing sorted approaches not all sorts can be processed by sorted unification due to the restrictions imposed on the sort theory. A consequence is that solv­ ing the puzzle with these approaches compares to solving the problem with the standard resolution method. We solved the problem on a Spare ELC workstation with 16MB using OTTER 2.2 and STOP 0.9 (Sorted The­ Orem Prover- a first prototype implementation of the new resolution method with sorts.). The table shows the number of clauses generated and the time spent by the provers in order to derive the query depending on the nesting depth of the function f in the query:

A second application concerns abduction. There are many applications for automated reasoning where ab­ ductive reasoning has to be applied. Of course, when using abduction one is interested in finite representa­ tions of answers. Demolombe and Farinas [Demolombe and Farinas, 1991] proposed an inference rule, called L-inference, which can be used to automatize abduc­ tive reasoning. The L-inference rule is a special reso­ lution rule. I will show that extending this rule with sorts allows the generation of finite answers to abduc­ tive queries, where the standard rule without sorts com­ putes infinite answers. Assume the query "Which as­ sumptions guarantee that Love(x, y) holds ?" is asked to the database ~ (see Section 1). Applying the stan­ dard rule amounts to compute all resolvents between the

and the clauses in ~- The literal L(x, y) is an extra literal introduced by Demolombe and Farinas method which is used to collect the instantiations made to the variables in the query literal. It is possible to derive infinitely many non-redundant clauses, e.g. clauses of the form

Applying L-inference to ~' the only possible resolution step uses clause ( 4) and results in

Thus the sorted answer is that two objects love each other if they are humans. This is the natural answer. The example demonstrates that the resolution method with sorts terminates in more cases and derives natural answers.

4 Discussion

The approach of Schmidt-SchauB [Schmidt-SchauB, 1989] extends Walther's work [Walther, 1987]. The res­ olution method with sorts is an extension of Schmidt­ SchauB's approach. If all declarations occur in uni t clauses and all negative sort literals can be compiled by COMP then all conditional parts of cws. terms are empty. If in addition all sorts S are non-empty, the resolution method with sorts is the same as Schmidt­ SchauB's order-sorted resolution calculus.

The framework presented by Frisch [Frisch, 1991] is more restricted than my approach. He separates the sort theory from the database. A sort theory is built from sort literals only and must be equivalent to a Horn theory. Sort literals are not allowed to occur with other literals in the database. As a consequence all sorts are a priori assumed to be non-empty. In addition, he does not answer how the sorted reasoning is to be performed, which in my approach is done by the notion of cws. terms and GSOUP.

The logic of Cohn [Cohn, 1992] also does not give an answer how sorted reasoning has to be performed (an oracle is assumed) . He imposes no restrictions on the occurrence of sort literals, but does not incorporate declarations occurring together with other literals in the sorted reasoning process. This leads to a calculus which consists of more inference rules than the usual resolu­ tion and factoring rule. In addition , unifiers which are not well sorted (with respect to Definition 2) have to be considered for the inference rules also. Therefore, the resolution method with sorts is much more restrictive in the number of applicable inference steps.

The same arguments that hold for Cohn, apply to the work of Beierle et al. [Beierle et al., 1992]. Al­ though he gives a fully developed calculus, his extended order-sorted unification algorithm is nothing else than unsorted unification plus the collection of a negative sort literal for each component of the unsorted unifier. Hence, his resolution method is also less restrictive in the num­ ber of applicable inference steps than the method pro­ posed in this paper.

Compared to the work of Weidenbach and Ohlbach [Weidenbach and Ohlbach, 1990] I switched from a static processing of the sort theory to a dynamic one. As a consequence the number of declarations considered by the unification algorithm has been reduced significantly. The new method also needs fewer inference rules. Thus the method presented in this paper is more restrictive in the number of applicable inference steps than our own previous work.

The frameworks of Stickel [Stickel, 1985] and Biirckert [Biirckert, 1991] propose methods for integrating theo­ ries into the resolution method. The resolution method with sorts is not an instance of these frameworks, be­ cause it is assumed that the theory is static during the deduction process. The sort theory £ changes during the deduction process. This allows for less inference rules and a more restricted calculus in the number of applica­ ble inference steps.

Sorted unification in our resolution method is unde­ cidable and of type infinitary (see Lemma 6). It is often argued that unification procedures having this property are not useful. But the result means that the sort the­ ory processed by sorted unification has this properties in general. Hence the question is whether it is more effi­ cient to process the theory by the unification procedure or by standard resolution. The notion of cws. terms pre­ vents sorted unification from performing inference steps which are performed by standard resolution. In general there may be infinitely many such steps. Thus using GSOUP is much more efficient than weaker unification algorithms combined with resolution.

5 Summary

Every standard first-order database can be thought of as a database with sorts where all variables have sort "any" (T). The algorithm COMP can be used to compile negative sort literals into variable restrictions. If COMP can save sort literals, applying the resolution method with sorts is more efficient than standard resolution. If COMP cannot save literals (aU variables have sort T) the resolution method with sorts derives exactly the same clauses than the standard resolution method.

The resolution method with sorts generalizes and im­ proves existing approaches to sorted reasoning.

The resolution method with sorts terminates in more cases than the standard resolution method. This is use­ ful for abductive reasoning, for example.

Acknowledgements

I would like to thank Alan M. Frisch, Renate Schmidt, and the reviewers for many helpful comments on this paper.