Automated Deduction by Theory Resolution

1 Introduction

lncorporating a theory into derived inference rules so that its axioms are never resolved upon has enormaus potential for re­ ducing the size of the exponential search space commonly en­ countered in resolution theorem proving. Theory resolution is a method of incorporating specialized reasoning procedures in a resolution theorem prover so tha~ the reasoning task will be ef­ fectively divided into two parts: special cases, such as reasoning about inequalities or about taxonomie information, are handled efficiently by specialized reasoning procedures, while more gen· eral reasoning is handled by resolution. The eonnection between the two reasoning components is made by having the resolution procedure resolve on sets of literals whose conjunction is deter­ mined to be unsatisfiable by the specialized reasoning procedure. The objective of research on theory resolution is the conceptual design of deduction systems that combine deductive specialists within the common framework of a resolution theorem prover.

Goneern has often been expressed about the inefl'ectiveness of applying resolution theorem proving to problems in artificial intelligence. Theory resolution is designed to partly address this concern by providing a means for incorporating specialized rea­ soning procedures in a resolution theorem prover. The division of Iabor achieved in the reasoning process by theory resolution is

1 This research was supported by the Defense Advanced Research Projects Agency under Contract N00039-84-K-0078 with the Naval Electronic Sys­ tems Command and was also made possible in part by a gift from the System Development Foundation. The views and conclusions contained in this document are those of the author and should not be interpreted as representative of the official policies, either expressed or implied, of the Defense Advanced Research Projects Agency or the United States govern­ ment. Approved for public release. Distribution unlimited.

Automated Deduction by Theory Resolution

Mark E. Stickel

Artificial lntelligence Center

SRI International and

Center for the Study of Language and Information Stanford University

intended to produce the dual advantages of improving the theo­ rem prover's performance by the use of more efficient reasoning procedures for special cases and of increasing the range of appli­ cation of the specialized reasoning procedures by including them in a more general reasoning system.

Past criticisms of resolution can often be characterized by their pejorative use of the terms uniform and 6yntactic. Theory resolution meets these objections head-on. In theory resolution, a specialized reasoning procedure may be substituted for ordi­ nary syntactic unification to determine unsatisfiability of sets of literals. Because the implementation of this specialized reason­ ing procedure is unspecified-to the theorem prover it is a "black box" with prescribed behavior, namely, able to determine unsat­ isfiability in the theory it implements-the resulting system is nonuniform because reasoning within the theory is performed by the specialized reasoning procedure, while reasoning outside the theory is performed by resolution. Theory resolution can also be regarded as being not wholly syntactic, since the conditions for resolving on a set of literals are no Ionger based on their being made syntactically identical, but rather on their being unsatisfi­ able in a theory, and thus resolvability is partly semantic.

Reasoning about orderings and other transitive relations is often necessary, but using ordinary resolution for this is quite inefficient . lt is possible to derive an infinite number of conse­ quences from a < b and (:r < y) II (!I < z) :::> (:r < z) despite the obvious fact that a refutation based on just these two formulas is impossible. A solution to this problern is to require that use of the transitivity axiom be restricted to occasions when either there are matches for two of its literals (partial theory resolution) or a complete refutation of the ordering part of the clauses can be found (total theory resolution).

An important form of reasoning in artilicial intelligence ap­ plications embodied in knowledge representation systems is rea­ soning about taxonomic information and property inheritance. One of our goals is to be able to take advantage of the efficient reasoning provided by a knowledge representation system by us­ ing it as a taxonomy decision procedure in a )arger deduction system. KRYPTON [4,13] represents an approach to construct­ ing a knowledge representation system composed of two parts: a terminological component (the TBox) and an assertional compo­ nent (the ABox) . For such systems, theory resolution indicates in general how information can be provided to the ABox by the TBox and how it can be used by the ABox.

2 Theory Resolution

We will now define the theory resolution operation and discuss various useful restrictions on theory resolution. We will Iimit our discussion to the variable-free "ground~ case of theory resolution, since Iifting to the generat case is straightforward.

We will assume the standard definitions of a term, an atomic formula (atom}, and a Iitera/. We will consider a clauae to be a disjunction of n ~ 0 literals. Ir n = 0, the clause is the empty clau&e 0 . If n = 1, the clause is a unit clauae. The disjunc­ tion connective V is assumed to be associative, commutative, and idempotent . The empty clause 0 is the identity element for V. We will generally make no distinction between a unit clause and the single Iiterat of which it is composed.

We will assume the standard definitions of an interpretation, an interpretation aatiafying or falaifying a formula or set of for­ mulas, and a formula or set of formulas being aatiafiable or un­ sati&jiable.

Any satisfiable set of formulas that we wish to incorporate into the inference process can be regarded as a theory.

Definition 1 A T -interpretation is an interpretation that satis­ fies theory T .

For example, in a theory of partial erdering ORD consisting of -.(x < x) and (x < 11) A (II < z) ~ (z < z), the predicate < cannot be interpreted so that a < a has value true or a < c has value fal&e if a < b and b < c both have value true. In a taxo­ nomic theory TAX including Bo11(z) ~ Per~on(z), Bo11(John) cannot have value true while Per~on(John) has value falae.

Definition 2 A set of clauses S is T -un1ati·fiable iff no T­ interpretation satisfies S. S is minimall11 T -un1ati·fiable ifl S, but no proper subset of S, is T-unsatisflable.

Definition S Let C,, ... , Cm (m ~ 1) be a set of nonempty clauses, Iet each C; be decomposed as K; V L; where K; is a nonempty clause, and Iet R,, . .. , Rn (n ~ 0) be unit clauses. Suppose the set of clauses K,, . .. , Km, R,, . . . , Rn ia Tunsatisfiable. Then the clause L1 V .. · V Lm V -.R1 V·· ·V -.R,. is a theory reaolvent u1ing theor11 T (I' -re1olvent) o{ C1, .. . , Cm. The theory resolvent is called an m-ar11 theory reao)vent. lt ia a total theory resolvent iff n · 0; otherwiae it ia partial. K1, .. . , Km is called the key o( the theory reaolution operation. For partial theory resolvents, R1, .. . , Rn is a aet of condition· for the T· unsatisliability of the key. The negation -.R1 V ···V -.R,. of the conjunction of the conditiona ia called the re1idue of the theory resolution operation. lt ia a narrow theory reao)vent ifl each K; is a unit clause; otherwiae it ia wide.

The partial theory resolution procedure permits total as weil as partial theory resolution operations. Similarly, the wide the­ ory resolution procedure permits narrow u weil u wide theory resolution operations.

Example 4 A set of unit clauses is unsatisflable in the theory of partial ordering 0 RD ifl it contains a chain of inequalitiea t1 < · · · < t"(n ~ 2) auch that either t1 ia the aame as t,. or -.(tt < t") is also one of the clauses. P ia a unary total narrow 0 RD-resolvent of ( a < a) V P. P V Q ia a binary total narrow ORD-resolvent of (a < 6) V P and (6 < a) V Q. P V Q V RV S is a 4-ary total narrow 0 RD-resolvent of ( a < 6) V P, ( 6 < c) V Q, (c < d) V R, and -.(a < d) V S. This can also be derived incrementally through partial narrow ORD-resolution, i.e., by resolving (a < b) V P and (b < c) V Q to obtain (a < c) V P V Q, resolving that with (c < d) V R to obtain (a < d) V P V Q V R, and resolving that with -.(a < d) V S to obtain P V Q V R V S.

Example 5 Suppose the taxonomic theory TAX includes a def· inition for fatherhood Father(x) s [Man(z)A 311Child(x,y)]. Then Father(Fred) is a partial wide theory resolvent of Child(Fred, Pat)V Child(Fred, Sand11) and Man(Fred). Also, 0 is a total wide theory resolvent of Child(Fred, Pat)V Child(Fred, Sandy), Man(Fred), and -.Father(Fred) .

We will explore some possible restrictions on the definition of theory resolution that make it practical to apply while preserving completeness.

In narrow theory resolution, only T-unsatisflability of sets of literals, not clauses, must be decided. Total and partial nar­ row theory resolution are both possible. In total narrow the­ ory resolution, the resolved-upon literals (the key) must be T­ unsatisfiable. In partial narrow theory resolution, the key must be T -unsatisfiable only under aome conditions. The negated con­ ditions are used as the residue in the formation of the resolvent.

We do not want to require the derivation of a11 partial narrow theory resolvents permitted by the definition. This would resu)t in the derivation of obvioualy unneceasary resolvents. For exam· ple, we could resolve (a < 6) V P and (c < d) V R, aince, under some conditions such as (6 < e) A (d < a), a < 6 and c < d are T-unsatisliable. lf we permit inferences from a < 6 and c < d, which have no terms in common, theory resolution would not be very useful. If resolving a < 6 and c < d were to actually Iead to a refutation-i.e., conditiona for their T-unaatisfiability do hold­ then some of these conditions, e.g., (6 < c) A (d < a), must have arguments in common with a < 6 and c < d. We should restriet partial theory resolution to cases in which the literals are suitably related.

To justify such pragmatica1ly necessary restrictiona on theory resolution, we offer the following criterion for the aelection of key sets of literals that providea a aufficient condition for the completeness of partial narrow theory reaolution.

In essence, the key ae)eetion criterion requirea that every T· unsatisfiable set of Iiterali have one or more subaet· key aets of literals that can be T-reaolved. For example, in theory ORD, in refuting sets of positive inequality literals, we might select only pairs of literals matehing z < 11 and 11 < z as key sets of literals. Thus, in refuting the set {a < b, b < c, c < d, d < a}, we would be permitted, for example, to resolve upon a < 6 and 6 < c, but not a < b and c < d. Key aeta of literals have one or more residues associated with them auch that every minimally T-unaatiaflable set includes a key with a reaidue that can be refuted by reaolving away the literals in the reaidue. With Iitera)· m·tching z < 11 and 11 < z selected, it ia aufficient to derive T·resolvents with residue x < z. For example, a < 6 and 6 < c can be T-reso)ved with a < c as the result. This can then be reso)ved with c < d to derive a < d that can be resolved with d < a to derive 0.

Key selection crlterlon.

• For any minimally T·unsatisflable set of literals S, there is at least one key aet of literals K such that K ~ S. K hu at least two literals (one Iitera) if S hu only one Iitera)). Each K is recognizable by the decision proeedure for T and will comprise the key (or pouible theory reaolution operation1, if clauses containing the key Iitera)· are preaent.
• For any such key set of literals K , there is at least one, possibly empty, residue set of literals R such that KU -.R is minimally T-unsatisfiable, where -.R denotes the set

{-,R,, ... ,-,R,.} when R = {R1 , ·· · ,R,.}. Each -,R is a set of conditions for the T-unsatisfiability of key set K. Each R is computed from K by the decision procedure for T and is used as a residue for theory resolution operations that resolve on key K.

• lt must be the case that, for some key set of literals K and associated residue set of literals R, (S - K) U {V R} is minimally T-unsatisfiable, where V R denotes the clause R1 V· ·· V R,. when R = {R" ... , R,.}. This ensures that key selection and residue computation will be suffi.cient for completeness-any T-unsatisfiable set of literals S has a T-resolvent using a key K ~ S and residue R computed from K such that the T-resolvent is Contradieted by the remaining literals S - K.

In total narrow theory resolution, we uniformly take the key K to be the entire minimally T-unsatisfiable set of literals S. The residue R is always empty.

In partial narrow theory resolution, we will try to minimize the number of residue sets of literals. Thus, for K = { a < b,b < c} we might have residues R, = {a < c}, R2 = {-,(c < xi), -,(x, < a)}, Rs = {-,(c < xt), -,(x, < xz), -,(xz < a)}, etc. However, only R, need be used, since, in the theory T, R1 implies every other ~- R, can be regarded as the strongest consequence of a < b and b < c in theory T.

The following theorem proves the completeness of narrow the­ ory resolution with arbitrary selec:tion of key sets of literals sat­ isfying the key selec:tion criterion.

Theorem 6 LetS be a T -umati&jiable &et of clauu&. Then there i& a refutation of S ( derivation of o from S) u&ing partial narrow theory re&olution with theory T for arbitrary &election of key 1t:t1 &atisfying the key ulection criterion.

Proof: lf o E S, then S is trivially refuted.

Otherwise we will prove the theorem by induction on com­ plexity measure c{S), where c{S) = {]S], k{S)), where ]S] is the number of clauses in S and k{S) ·is the e:rceu Iitera/ parameter [1] . The excess Iitera! parameter is defined tobe the number of literals (i.e., Iiterat oceurrences) in S minus JSJ. The ordering of c(S) is defined by c{Sl)-< c{S2) ifl' ]S,] < ]S2], or ]51]= ]S2] and k(St) < k(S2).

Gase c(S) = {m,O). Every elause must be a unit elause. Because S is T-unsatisfiable, it must inelude a minimally T­ unsatisfiable subset S'.

Subcase ]S'] ~ 2. By the key selec:tion criterion, S' must be selec:ted as a key. The empty elause o is deriv.able in a eingle unary or binary T-reeolution step from S' and hence from S.

Subcase JS'J > 2. By the key eeleetion eriterion, there exists a key K ~ S' with ]K] ~ 2 and (possibly empty) residue R euch that S" = (S'-K) U {VR} is minimally T-unsatisfiable. c{S") -< c{S') ~ c{S). Thus, by the induction hypothesie, o is derivable from S". Since V R is a T·resolvent of K s;; S, o is derivable from S.

Gase c{S) = {m,n), n > 0. Select a nonunit clause GE S. Decompose G into unit clause A and clause B, i.e., G = A VB. Because S is T-unsatisfiable, both s_,.. = (S- {G}) U {A} and SB= (S- {G}) U {B} are T-unsatisfiable. Both c{S_,..)-< c{S) and c(SB) -< c(S). Thus, by the induction hypothesis, there must exist derivations of o from each of S A and SB.

Imitate the derivation of 0 from SB, using G instead of B. The result will be a derivation of either o or A from S. In the latter case, extend the derivation of A from S to a derivation of 0 from S by appending the derivation of 0 from SA. I

Corollary 7 Let S be a T-un&atj,fiable &et of clauses. Then there i& a refutation of S (derivation of 0 from S) using total narrow theory resolution with theory T.

Although the theorem proves completeness of narrow theory resolution, its proof does not preelude the need for tautologies in a refutation. lndeed, it is the case that tautologies may have to be retained for a refutation to be found.

Example 8 Let T be the theory in which P, Q, and Rare all equivalent . Let S be {P V Q V R, -,p V -,Q V -,R}. There is a single-step wide T-resolution refutation of S. However, although there do exist refutations of S by narrow T -resolution, all require retention of tautologies, since all narrow T-resolvents of PVQV R and -,p V -,Q V -,R are tautologies.

Finally, note that heuristic restrictions of theory resolution (such as discarding all tautologies, not recognizing all cases of T-unsatisfiability, or not computing all residues), though incom­ plete, may be very useful in practice.

3 Examples of Theory Resolution

Theory resolution is a procedure with substantial generality and power. Thus, it is not surprising that many specialized reason­ ing procedures can be viewed as instances of theory resolution, perhaps with additional constraints governing which theory re­ solvents can be inferred. We believe that the success of these specialized reasoning procedures helps to validate the concept of theory resolution.

First of all, we should note that there is a relationship be­ tween theory resolution and hyperreaolution. Although fur­ ther constraints {e.g., on the polarity of the literals) are often prescribed, the essence of hyperresolution is the derivation of L, V ··· V Lm V R from the electron clauses K; V L;, where K; is a Iitera! and L; is a [possibly empty] clause and the nucleus clause -,K, V··· V -,Km V R, where R is a (possibly empty] clause. This corresponds to a theory resolution operation using theory T, where ..,K, V··· V-.Km V R is a consequence ofT, K1, ... , Km is the key set of Iiterals, and R is the residue.

Theory resolution is also related to procedural attach­ ment, whereby expressions are "evaluated· to produce new ex­ pressions. Ordinary procedural attachment can be regarded as unary theory resolution. Theory resolution in generat can be con­ sidered as an extension of the notion of procedural attachment to sets of literals. Where ordinary procedural attachment permits the replacement of 2 < 3 by true, theory resolution, in effect, can attach a procedure to the < relation that permits derivation of a < c from a < 6 and 6 < c.

Two previous refinements of resolution that resemble partial theory resolution are Z-resolution and U-generalized resolution.

Dixon's Z-resolution (5] is essentially binary total narrow theory resolution with the restriction that T must consist of a finite deductively closed set of 2-clauses (clauses with length

2). This restriction does not permit inclusion of assertions like -,Q(x) V Q(f(x)), -,(x < x), or (x < y) II (y < z) :::> (x < z), but does permit efficient computation of T-resolvents (even allowing the possibility of compiling T to LISP code and thence to ma­ chine code) . Z-factoring and Z-subsumption operations are also defined.

Harrison and Rubin's U-generalized resolutlon [7] is es­ sentially binary partial narrow theory resolution applied to sets of clauses that have a unit or input refutation. They apply it to building in the equality relation, developing a procedure similar to Morris's E-resolution [10] . The restriction to sets of clauses having unit or input refutations eliminates the need for factor­ ing and simplifies the procedure, but otherwise Iimits its appli­ cability. No effort was made in the definition of U-generalized resolution to Iimit the applicability of T-resolution to reasonable cases (e.g., formation of an ORD-resolvent of o < 6 and c < d is permitted by the definition).

The linked lnference prlnclple by Wos et al. [22] is related to theory resolution in concept and purpose. The linked infer­ ence principle is a somewhat more conservative extension of res­ olution than theory resolution, since it stipulates that the theory will be built in by means of clauses designated as linking clauses. Theory resolution, on the other band, allows the theory to be incorporated as a "black box" that determines T-unsatisfiability questions in an unspecified manner. This facilitates the use of other systems, which do not rely upon resolution or clause rep­ resentation, to build in theories. Nevertheless, many instances of theory resolution can be usefully implemented in the manner of the linked inference principle. Since the implementation pro­ poaal for the linked inference principle is more concrete, Wos et al. have expended comparatively more efl'ort in determining how inference using the linked inference principle is to be controlled, including defining linked variants of resolution refinements such as unit-resulting resolution and hyperresolution.

We have already suggested the importance of theory resolu­ tion for taxonomlc rea.onlng. This is being explored in the KRYPTON knowledge representation system. Figure 1 contains a nearly verbatim transcription of a proof using KRYPTON-style reasoning. The problern is to prove that, if Chris has no sons and no daughters, then Chris has no children.

The terminological information used in this problern through theory resolution includes the statements that boys are persons whose sex is male; girls are persons whose sex is female; "no-sons" are persons all of whose children are girls; "no-daughters" are per­ sons all of whose children are boys. Relevant portions of this in­ formation are included in Formulas 1-6, whieh are used to define what theory resolution operations are possible. Ir complements of the first two atoms of each formula can be found, they can be resolved upon, and the remaining part of the formula, if any, would be derived as the residue. Thus, Formula 1 expresses the unsatisfiability of Boy(John) and -.Peraon(John). Formula 5 permits the derivation of Girl(Sondy) from NoSon(Mory) and Child(Mory, Sondy). These formulas behave similarly to linking clauses in linked inference [22].

The assertional information used in this problern includes the information that every person has a sex; males and females are disjoint ; Chris has no sons and no daughters. From these facts, and the built in terminological information, a refutation is com­ pleted starting with the negation of the desired conclusion that Chris has no children . .Jk1 and ak2 are Skolem functions.

The following table compares the statistics for proofs completed with and without Formulas 1-6 built in through theory resolution. The proof strategies used and meaning of the statis­ tics are essentially the same as described in Section 4

There is a noticeable improvement resulting from using theory resolution, but because the problern is so small, the difference is not large. Harder problems (Iike the one in Section 4) can be used to demonstrate much greater improvement .

Theory resolution for taxonomic reasoning also incorporates many elements of reasoning in a many-sorted loglc. For ex­ ample, in Walther's I:RP-calculus (many-sorted resolution and paramodulation) [17,19], sort declarations, subsort relationships, and sort restrictions on clauses are all incorporated into the uni­ fication procedure, and eliminated from the clauses in the state­ ment of a problem. Thus, the I:RP unification procedure imple­ ments a theory of sort information.

4 Experimental Results

Although the relationship of theory resolution to many other extensions of resolution and experience with numerous small ex­ amples support the practical value of theory resolution, we will not elaborate on these, but will rather bolster our claim with an examination of experimental results for "Schubert's Steamroller" challenge problem.

Schubert's steamroller problern (annotated with formula numbers) is

(1-5) Wolves, foxes, birds, caterpillars, and snails are animals, and (7-11) there are some of each of them. Also (12) there are some grains, and (6) grains are plants. (13) Every animal either likes to eat all plants or all animals much smaller than itself that like to eat some plants. (14) Caterpillars and snails are much smaller than birds, which are much smaller than foxes, which in turn are much smaller than wolves. (15) Wolves do not like to eat foxes or grains, while (16) birds like to eat caterpillars but (15) not snails. (17) Caterpillars and snails like to eat some plants. Therefore (18) there is an animal that likes to eat a grain-eating animal.

We present statistics on several solutions of Schubert's steam­ roller problern found by our theorem prover (15]. The first is a proof that does not use theory resolution; the second is a proof using theory resolution to implement the taxonomic information in the problern (Formulas 1-6); the remaining proofs show the re­ sults of using theory resolution to build in each of Formulas 14-17 successively.

The same strategy was used for all of the proofs. Nonclausal connection-graph resolution was the principal inference rule. Fac­ toring was not employed. Pure, variant , and tautologous formu­ las were eliminated. Single Iitera! formulas were used for both forward and backward demodulation.

Heuristic search, guided by a simple weighted function of the deduction Ievel of the parents and the expected size of the re· solvent, was ·Used to decide which inference operation should be perlormed next. The set of support strategy (with only For­ mula 18 supported) and an ordering strategy that designated which atoms in a formula could be resolved upon were used to Iimit the number of alternative inference operations.

In using theory resolution, connection graph links were cre· ated from key sets of literals in the theory being incorporated. Formulas 1-ß and 17 were implemented by binary total narrow theory resolution links and Formulas 14-16 were implemented by 3-ary total narrow theory resolution links. For example, Wolf(t) and ..,Animal(t) could be linked, and Bird(tt) , Snai/(t2), and Like6·to-eat(tt, t2) could all be linked. Theory resolution was also used in demodulation-e.g., Wo/f(t) could be used to de­ modulate Animal(t) to true.

Following are the statistics for. the various solutions of Schu­ bert's steamroller problem. Included in the statistics are the number of formulas inputted to the theorem prover, the number of formulas derived in the course of searching for a proof, the number of inputted and derived formulas still present when a proof was found, the number of successful unification attempts during the search for a proof (including unification during link inheritance), the time required for the proof (on a Symbolics 3600 personal LISP machine), and the length of the proof in resolution steps.

Also included in the table are stat1stics we know for solu­ tions of Schubert 's steamroller problern by other systems. Unfor­ tunately, use of slightly different axiomatizations, e.g., whether "grain-eating animal" is interpreted as an animal that eats some grain (our work, see [16]) or every grain [18], makes statistics for thesedifferent solutions not strictly comparable. We will publish a more detailed comparison of solutions later.

The MKRP solution was done by Walther [20] using the Mark­ graf Karl Refutation Procerlure [3] . This proof relied heavily on the MKRP TERMINATORmodule [2], which is essentially a very fast procedure for finding unit refutations . A superior proof by Walther [18] used his L:RP calculus [17,19] in the MKRP sys­ tem to perform many-sorted resolution on a much reduced set of clauses. This proof also used the TERMINATOR module, but , given the reduction in the number of clauses and literals made possible by using many-sorted resolution and its restrictions on unification, here its use was not essential to finding a solution with reasonable effort. MKRP is written in INTERLISP and was run on a Siemens 7760 computer.

Our first theory resolution proof, in which only the taxonomic information of Formulas 1-6 is incorporated, has some similar­ ity to a many-sorted resolution proof. In the MKRP ERP proof, Wolf, Fox, Bird, Caterpillar, and Snail were declarcd tobe sub­ sorts of sort Anima/ and Grain was declared tobe a subsort of sort Plant. The unification algorithm was restricted so that a variable can be unified with a term if and only if the term is a subsort of or equals the sort of the variable. For building in just this taxonomic information, many-sorted resolution is stronger than this particular instance of theory resolution. Although theory resolution bandies the sort literals more effectively than ordinary resolution, many-sorted resolution dispenses with them entirely. Also, many-sorted resolution is used to build in the sort infor­ mation for Skolem constants and functions so that , in Schubert's steamroller problem, Formulas 7-12 are supplanted by type dec­ larations.

The ITP solution was found by the automated reasoning sys­ tem ITP (written in PASCAL) developed at Argonne Nat ional Labaratory [9]. This solution used qualified hyperresolution [8,21] and was completed in about six minutes on a VAX 11/780 computer [12] . Like the theory resolution and MKRP L:RP solu­ tions, this solution treated the taxonomic sort information in the problern specially. In qualified hyperresolution, some li terals in a clause can be designated as qualifier literals that contain "con­ ditions of definition" for terms appearing in the clause. Qualifier literals are ignored during much of the inference process- e.g., a clause consisting of a single nonqualifier Iitera! and some qualifier literals is handled as if it were a unit clause- with the conditions imposed by the qualifier literals checked only after the qualified terms are instantiated. Thus, sort restrictions can be specified in qualifier literals and deductions can be perlormed using only the nonsort information. The deductions are then subjected to verification that terms are of the correct sort.

5 Conclusion

Theory resolution is a set of complete procedures for incorporat­ ing decision procedures into resolution theorem proving in first­ order predicate calculus. Theory resolution can greatly decrease the length of proofs and the size of the search space. Theory resolution is also a generalization of several other approaches to building in nonequational theories.

We are implementing and testing forms of theory resolu· tion in tbe deduction·system component of the KLAUS natural· language-understanding system [6,15]. This system demon· strated substantial improvement in performance when theory res· olution was used on Schubert's steamroller challenge problem. The KRYPTON knowledge representation system is also applying the ideas of theory resolution to combine a terminological rea· soning component and an assertional reasoning component (for which they are also utilizing the KLAUS deduction system).

Theory resolution is a proeedure with substantial power and generality. It is our hope that it will serve as a base for the theo­ retical and practical development of a methodology for combining the general reasoning capabilities of resolution theorem·proving programs with more efficient speeialized reasoning procedures.

One important area for further research on theory resolution is finding restrictions on the need for retention of tautologies and determining compatibility with other resolution reflnements.

Another important researeh question is handling eombina· tions of theories (beyond the trivial case of totally disjoint the· ories). Successful combining of multiple deductive specialists within a resolution framework awaits further development in this area. The work of Nelson and Oppen [11] and Shostak [1.C] on combining quantifier free theories may be relevant.

Acknow ledgments

The author would like to thank Mabry Tyson, Richard Waldinger, and Christoph Walther for their very useful comments on an ear· lier draft of this paper.