--- title: "Ordering-Based Strategies for Horn Clauses" authors: - "Nachum Dershowitz" doi: "" url: "https://ijcai.org/proceedings/1991/18" pdf: "https://ijcai.org/proceedings/1991/0018.pdf" venue: "Proceedings of the Twelfth International Joint Conference on Artificial Intelligence" year: 1991 pages: "118-124" track: "Automated Reasoning" keywords: --- # Ordering-Based Strategies for Horn Clauses Nachum Dershowitz *Proceedings of the Twelfth International Joint Conference on Artificial Intelligence*, pages 118-124. ## Abstract Two new theorem-proving procedures for equational Horn clauses are presented. The largest literal is selected for paramodulation in both strategies, except that one method treats positive literals as larger than negative ones and results in a unit strategy. Both use term orderings to restrict paramodulation to potentially maximal sides of equations and to increase the amount of allowable simplification (demodulation). Completeness is shown using proof orderings. ## Full text ## 1 Introduction The completeness of positive-unit resolution for sets of Horn clauses p1 /1. · · · /1. Pn => Pn+l is well-known. An advantage of a unit strategy is that the number of literals in clauses never grows; it suffers from the disadvantage of being a bottom-up method. Ordered resolution, in which the literals of each clause are arranged in a linear order > and only the largest literal may serve as a resolvent, is also complete for Horn clauses [Boyer, 1971]. The purpose here is to design Horn clause strategies that make more comprehensive use of orderings in controlling inference. A conditional equation is a universally-quantified Horn clause in which the only predicate symbol is equality (:=) . Conditional equations are important for specifying abstract data types and expressing logic programs with equations. We write such a clause in the form e1 /1. · · · /1. en => s := t (n ~ 0), meaning that the equality s := t holds whenever all the equations ei, called conditions, hold. If n = 0, then the (positive unit) clause, s := t, will be called an unconditional equation. Horn clauses with both equality and non-equality literals can be expressed as conditional equations with equality literals only by turning each nonequality atom I into a Boolean equation I := T, for the truth constant T. A conditional equation e1 /1. ... /1. en => s := t is valid for E iff s := t is valid for E U { e1 , . .. , en}; hence, proving validity of conditional equations reduces to proving validity of unconditional ones. ·This research supported in part by the National Science Foundation under Grant CCR-9007195. Positive-unit resolution, or any other complete varia­ tion of resolution, could be used to prove theorems in equational Horn theories (the equality axioms, includ!ng functional reflexivity, are Horn), but the cost of treatmg equality axioms like any other clause is prohibitive. For this reason, special inference mechanisms for eq.\_uality, notably paramodulation [Robinson and Wos, 19691, have been devised. In the Horn case, a unit strategy can be combined with paramodulation [Henschen and Wos, 1974; Furbach, 1987]. In this paper, we describe two complete theorem­ proving method~ for . equational Horn ~heories. J:.s in lHsiang and Rusmow1tch, 1986; Kounahs and Rusmow­ itch, 1987; Zhang and Kapur, 1988; Rusinowitch, 1989; Bachmair and Ganzinger, 1990; Nieuwenhuis and Orejas, 1990], our goal is to minimize the amount of paramodu· lation, while maximizing the amount of simplification­ without threatening completeness. Orderings, described in detail in Section 2, are used to choose which literals participate in a paramodulation step, and which side of an equality literal to use. They utilize orderings of terms and atoms to restrict inferences, and are generalizations of ordered completion [Bachmair et a/., 1986; Hsiang and Rusinowitch, 1987], an "unfailing" extension of the "completion procedure" in [Knuth and Bendix, 1970] for unconditional equational inference. Completion operates on asymmetrical equations, that is, on rewrite rules, and has as its goal the production of confluent (Church-Rosser) systems of rules that can be used to decide validity. To achieve this, the larger sides of rules are overlapped on (non-variable) subterms of each other, producing equations that are called "critical pairs". Brown [1975] and Lankford [1975] first suggested combining completion for oriented unconditional equa­ tions, with paramodulation for unorientable ones ~nd resolution for non-equality atoms. Paul [1986] studied the application of completion to sets of Horn clauses with equality. Completion was extended to conditional equations by Kaplan [1987], who turns equations into rules only if they satisfy a certain "decreasingness" condition. The problem is that the critical pair of two decreasing rules can easily be nondecreasing. Like standard completion , both these methods may fail on account of inability to form new rules. Kounalis and Rusinowitch [1987] suggested narrowing conditions to achieve completeness. Recently, several restrictions ofparamodulation based on term orderings have been proposed for the full first-order case, including [Zhang and Kapur, 1988; Rusinowitch, 1989; Bachmair and Ganzinger, 1990]. For a survey of rewriting, see [Dershowitz and Jouannaud, 1990]. Section 3 presents a set of inference rules that severely restricts resolution with paramodulation by incorporat­ ing an ordering on (atoms and) terms. Limiting inference partially controls growth; keeping clauses fully simplified stunts growth even further. Such restrictions are of paramount importance in any practical theorem prover, but their (refutational) completeness has been difficult to establish. For our completeness proofs, sketched in Section 4, we adapt the proof-ordering method of [Bachmair et al., 1986] to conditional proofs. Section 4.1 demonstrates the completeness of a unit strategy (sug­ gested in [Dershowitz, 1990]) and Section 4.2 considers a strategy based on conditional completion of decreasing rules. Proof orderings allow us to limit narrowing to negative literals in the unit strategy, something that appears impossible with the recent transfinite-tree proof method used in [Hsiang and Rusinowitch, 1987]. The crux of our proof normalization argument is the observation that any conditional equational proof not in "normal form" must either have a "peak", that is, two applications of equations such that the middle term is the largest of all those involved and all subproofs are in normal form, or a "drop", that is, an application of an equation (or reflexivity of equals) to an instance of a condition in which all subproofs are in normal form. The strategies are designed to eliminate peaks and drops, thereby reducing the complexity assigned to the proof. Section 5 concludes with a short discussion. ## 2 Simplification Orderings Let T be a set of (first-order) terms, with variables taken from a set X, and g be its subset of ground (variable­ free) terms. If t is a term in T, by tl,.. we signify the subterm oft rooted at position 'll'"j by t[s],.., we denote the term t with its subterm tl,.. replaced by some term s. Term orderings are of central importance in the proposed methods. A total ordering > on ground terms g is called a complete simplification ordering [Hsiang and Rusinowitch, 1987] if it has (a) the "replacement property", s > t implies that any term u[s),.., with subterm s located at some position .,..., is greater under > than the term u[t),.. with that occurrence of s replaced by t, and (b) the "sub term property", t ?: t 1,.. for all subterms tl,.. of t . Such a ground-term ordering must be a well-ordering (see [Dershowitz, 1987]). A completab/e simplification ordering on all terms T is a partial ordering >- (c) that can be extended to a complete simplification ordering > on ground terms, such that (d) s >- t implies that su > tu for all ground substitutions u. Furthermore, we will assume (e) that the constant T is minimal in >- . Imagine a total ordering of atoms and with no equa­ tions, per se. The method of Section 4.1, then, is just selected positive-unit resolution, in which the largest negative literal is chosen. The appropriate inference rule would be expressed as: where u is the most general unifier (mgu) of I and s . Here, the positive unit clause I-:::::. T is resolved with the negative literal s -:::::. T in the clause q 1\ s -:::::. T => u -:::::. T , and produces a new Horn clause qu => uu -:::::. T . The new clause is a logical consequence of the two given clauses, since su = lru, where r renames variables in I so that it shares none with s. The clause would be generated only when s > q, by which we mean that sis the largest negative literal in its clause. A total simplification ordering on non-ground literals is not actually possible (which is why the ordering of the parent clause is inherited in ordered resolution), but can be approximated by a partial ordering. If only a partial ordering >- is given, we resolve negative literals that are potentially maximal. That is, we apply the above rule if su f!. qu, or, in other words, if the instance su of s created by resolution is not necessarily smaller than the other instantiated negative literals. Since some of the rules we consider delete or simplify antecedent clauses, the above format for inference rules, with the equations that participated in the inference also appearing as part of the consequent, is advantageous. Suppose E is a set of Horn clauses in conditional equation form. To handle equality literals I -:::::. r , we need to unify at subterms of conditions, not just at the literal level. Note that whenever we refer to equations in a set, we mean that it, or the symmetric equation (with I and r exchanged), or a variant with variables renamed uniformly, actually appears in the set . With that in mind, if I unifies with a non-variable subterm si,.. of a maximal term s in a condition s -:::::. t of a conditional equation q 1\ s -:::::. t => u -:::::. v, then a new Horn clause is created by applying the most general unifying substitution u to the conditional equation , and then replacing lu with ru, as per the unit clause I -:::::. r. The conditions ensure that su is the (potentially) larger side of the condition that is being paramodulated into and that the replacement yields a (potentially) smaller condition. ## 3 Inference Rules We formulate our theorem-proving procedure as an infer­ ence system operating on a set of conditional equations, and parameterized by a completable ordering >- . We define a symmetric binary relation +-+, for a particular set of conditional equations E , as the smallest relation satisfying t[lu],.. +-+ t[ru],.. for all u1 -:::::. v1 1\ · · · 1\ Un -:::::. Vn => I -:::::. r in E such that u.;u +-+* v; u for each i, where +-+* is the reflexive-transitive closure of +-+. This relation corresponds to "substitution of equals" according to the axioms in E . We also define a decreasing rewrite relation -+ E on terms T . An instance pu => uu -:::::. vu of a conditional equation is "decreasing" if ttO' >- VO' in the completable ordering and the proofs of the conditions only involve terms smaller than uO'. We write u -e v (with respect to a partial ordering >-), if u +-+e v using a decreasing instance of e. For unit equation e, -e is just the intersection of +-+e and >-. Decreasingness is essentially the same condition as imposed on conditional rewrite rules by the completion-like procedures of [Kaplan, 1987; Ganzinger, 1987]. In these methods, superposition is used when the left-hand side is larger than the conditions; narrowing, when a condition dominates the left-hand side. As theorem provers, however, they are refutationally incomplete, since they make no provision for "unorientable" equations s ::= t such that s 'f t and t 'I s. The inference rules we present may be classified into three "expansion" rules and four "contraction" rules. Contraction rules significantly reduce space require­ ments, but make proofs of completeness much more subtle. Superposition (i.e. oriented paramodulation of posi­ tive equational literals) is performed only at non-variable positions ( ul,.. fl. X). Only positive equations are used in this rule, and only in a decreasing direction (up f< pp, qp). Either side of an equation may be used for superposition, but only if, in the context of the paramod­ ulation, it is potentially the largest term involved (up f< vp, up[rp],..). Note that the two conditional equations may actually be the same (except for renaming). Here and later, when a rule refers to a clause of the form q => u ::= v, an unconditional equation ( u ::= v) is also intended. When both participating equations are unconditional, an unconditional "ordered" critical pair is generated. We need, additionally, a rule that paramodulates into maximal negative literals: Narrow: Whenever this or subsequent rules refer to a conditional equation like q 1\ s ::= t => u ::= v, the intent is that s ::= t is any one of the conditions and u is either side of the implied equation. Superpose: The last expansion rule in effect resolves a maximal negative literal with reflexivity of equals (x ::= x): Reflect: The contraction rules all simplify the set of conditional equations. The first deletes trivial conditional equations: The next rule allows for deletion of conditions that are trivially true: The last two contraction rules use decreasing instances to simplify other clauses. One rule simplifies conditions; the other applies to the equation part. In both cases, the original clause is replaced by a version that is logically equivalent, assuming the rest of E. Simplify: Compose: EU{p => u == v } EU{q => u == v } if p - 8 q EU{ q => u::=v} Eu { q => w::=v} if { U -p==:>l~r w, P => l ::= r E E v >- u V (u ::= v) t> (l ::= r) By u ::= v t> l ::= r we mean that the larger of u and v, say u, is strictly greater than the larger side of I ::= r, say I, in the encompassment ordering (wherein a term is larger than its proper subterms and smaller than its proper instances), or that u = l but v is strictly greater than r under >-. This allows the larger side of an equation to be simplified by a more general equation, and the smaller side to be rewritten in any case. We use the notation E 1- E' to denote one inference step, applying any of the seven rules to a set E of conditional equations to obtain a new set E'. The inference rules are evidently sound, in that the class of provable theorems is unchanged by an inference step. ## 4 Strategies Let > be any complete simplification ordering extending the given partial ordering >-. A proof of an equation s ::= t between ground terms (any variables in s and t may be treated as Skolem constants) is a "derivation" of m + 1 terms (m 2:: 0), each step tk <-+ tk+1 of which is either trivial (tk+1 = tk), or else is justified by a conditional equation ek in E, a position 7rk in tk, a substitution Uk for variables in the equation, and subproofs Pk (of the same form) for each conditions '-'k,jUk ~ Vk ,jUk of the applied instance ekuk. Steps em­ ploying an unconditional equation do not have subproofs as part of their justification. (By the completeness of positive-unit resolution for Horn clauses, any equation s ~ t that is valid for a set E of conditional equations is amenable to such an equational proof.) We use+- for the inverse of-+, and -+· and +-· for the reflexive-transitive closures of -+ and +-, respectively. By a peak, we mean a proof segment of the form s +- u -+ t; by a valley, we mean a proof segment of the form u -· w -· t; by a drop, we mean a steps-+ t with valley subproofs; a plateau is a trivial subproof of form s +-+ s. The depth of a proof is the maximum nesting of subproofs; it is one more than the maximum depth of its subproofs. ## 4.1 Unit Stratgey The inference rules of the previous section are designed to allow any equational proof to be transformed into normal form. A strategy based on these rules is complete if we can show that, with enough inferences, any theorem has a normal-form proof. For the unit strategy, a normal-form proof is a valley proof of depth 0. That is the same as saying that a normal-form proof has no peaks, no drops, and no plateaus. Normal-form proofs may be thought of as "direct" proofs; in a refutational framework the existence of such a proof for 8 ~ t means that demodulation of s and t using positive unit equations suffices to derive a contradiction between the Skolemized negation s' '/!. t' of the given theorem and X~ X. We must demonstrate that for any proof s +-+ · t of s ~ t in Eo, there eventually exists an unconditional valley proof s -+· w +-· t. In the unit strategy, only expansions involving an unconditional equation are necessary. Specifically, . both equations used by superpose are unconditional and the positive literal used in narrow is a unit. Were it not for contraction rules, it would be relatively easy to show that narrow and reflect eventually provide an unconditional proof of s ~ t, and that superpose eventually turns that into a valley. We call an inference "fair" if all persistent superpo­ sitions of unit clauses, narrowings via unit clauses, and reflections have been considered: Unit Strategy: An inference sequence Eo 1- E1 1- · · · is fair with respect to the unit strategy if where Eoo is the set lim infi Ei = Ui2:0 ni2:i Ei of persisting conditional equations and exp 1 (E00 ) is the set of conditional equations that may be inferred from persisting equations by one application of superpose with p and q empty, narrow with p empty, or reflect. Theorem 1. If an inference sequence Eo 1- E1 1- · · · is fair for the unit strategy, then for any proof of s ~ t in Eo, there is a normal-form proof of s ~ t in E00 · This is shown by transfinite induction on proofs. The term ordering > is extended to the transitive closure of it and the proper subterm ordering. This in turn is extended to equations by considering the equation as a multiset of two terms, and using the multiset extension of this ordering. (In the multiset ordering [Dershowitz and Manna, 1979], a multiset is decreased by replacing an element with any finite number of smaller elements.) An equation is greater than a term if and only if one of its sides is. Conjunctions of equations are compared as multisets of these multisets, and a conjunction is larger than a term if one of its conjuncts is. Proofs are measured in the following way: Consider a step in a ground proof or its subproofs, where e is the conditional equation q ~ I ~ r justifying the step, u is the substitution, and s is the larger of s and t (in the complete simplification ordering > extending >-). To each such step, we assign the weight Steps are compared in the lexicographic ordering of these pairs. The first components of pairs are compared in the multiset extension of the ordering on conjunctions and terms described above. (Note that 8 is always greater or equal to lu, and that for decreasing instances it is also greater than qu.) Second components are compared using the extension l> of the encompassment ordering described earlier . Proofs are compared in the well­ founded multiset extension of the lexicographic ordering on steps. We use ~ to denote this proof ordering. 'It can be shown by standard arguments (see, e.g., [Dershowitz and Jouannaud, 1990]) that ~ is well-founded. Note that if s -+e t, then the cost of this step is always greater than the cost of the steps in its subproofs. Also, if s -+ t -+ u, then the cost of the first step is larger than that of the second. We need to show that inferences never increase the complexity of proofs and, furthermore, that there are always inferences that can decrease the complexity of non-normal proofs. Then, by induction with respect to ~, the eventual existence of a normal-form proof follows. Lemma 1. If E 1- E', then for any proof P in E of an equation s ~ t, there exists a proof P' in E' of s ~ t, such that P ~ P' or P = P'. This is established by consideration of the effects of each contracting inference rule that deletes or replaces equations, since for expansion rules, E ~ E', and we can take P' = P . The conditions imposed on compose are essential for showing a decrease in ~. (A more general contraction rule would simply allow deletion of any equation that admits a smaller proof vis-a-vis ~. ) Lemma 2. If P is a non-normal-form proof in E, then there exists a proof P' in E U exp 1 (E) such that P ~ P'. The argument depends on a distinction between "non­ critical" subproofs, for which there is a proof P' in E itself, and "critical" subproofs, for which equations in exp 1 (E) are needed. A peak where t = w[lu],..[ur]p, is critical if the position 1r is at or below the position p in w at which u ~ v is applied, but not at or below a position corresponding to any variable in u, or (symmetrically) if p falls within the non-variable part of the occurrence of I in w. Similarly, a drop t -;,~e" t" is critical if the first or last step of one of the subproofs for qu takes place within the non-variable part of the condition q. Since any proof must have at least one subproof of depth 0, any non-normal proof must have a plateau, an unconditional peak, or a drop of depth 1 with (unconditional) valley subproofs. Thus, we need not worry about peaks involving a conditional rule, nor drops in which the proof of some condition is not unconditional. All plateaus can be spliced out. Criti­ cal unconditional peaks, critical drops with non-empty unconditional valley subproofs, and drops with empty proofs of conditions can each be replaced by a smaller proof, using the conditional equation generated by a required application of superpose, narrow, or reflect inference, respectively. Narrowing can be restricted to the maximal side of the maximal condition, since a drop with non-empty subproofs must have a step emanating from the larger side of its largest condition. Non-critical unconditional peaks t' +- t - t" have alternative, smaller proofs t' -· t +-* t" in E by the version of the Critical Pair Lemma in [Lankford, 1975]. Consider a non-critical drop w[uu] +-+q11~u11 ::=:v" w[vu], with unconditional sub proof pu - p' - · p" +-· p"', where pu is no smaller than any other term in the subproof qu. Suppose p has a variable z at position 1r and the first step applies within the variable part pi,... That is, pu = pu[zu],.. - pu[r],.. = p'. Let T be the same substitution as u except that T : z ...,... r. There is a smaller proof (smaller, vis-a-vis ~) in E: w[uu] +-* w[ur] +-+q 11~u11~v 11 w[vr] -· w[vu]. Any rewrites zu - r that need to be added to turn a proof of qu into a proof of qr are also smaller. Theorem 1 follows: If 8 ~ t is provable in Eo, then (by Lemma 1) it has a proof Pin the limit E 00 · If P is non-normal, then (by Lemma 2) it admits a smaller proof P' using (in addition to Eoo) a finite number of equations in exp 1 (E00 ). By fairness, each of those equations appeared at least once along the way. Subsequent inferences (by Lemma 1) can only decrease the complexity of the proof of such an equation once it appears in a set Ei (and has a one-step proof). Thus, each equation needed in P' has a proof of no greater complexity in Eoo itself, and hence (by the multiset nature of the proof measure), there is a proof of 8 ~ t in Eoo that is strictly smaller than P. Since the ordering on proofs is well-founded, by induction there must be a normal proof in Eoo. ## 4.2 Decreasing Strategy In the above method, only unconditional equations are used for superposition and narrowing. An alternative is to design an inference system that distinguishes between decreasing and nondecreasing non-unit clauses. We give here a method based on the incomplete completion method in [Ganzinger, 1987]. The required inferences (using superpose and narrow) are again a stringent restriction of paramodulation. For t.he decreasing method, we redefine a normal-form proof of 8 ~ t to be a valley proof in which each sub proof is also in normal form and each term in a subproof is smaller than the larger of 8 and t; see [Dershowi tz and Okada, 1988]. Any non-normal-form proof has a peak made from decreasing instances with normal-form subproofs, or has a nondecreasing step with normal­ form subproofs, or has a trivial step. The Critical Pair Lemma of [Kaplan, 1987] for decreasing systems can be adapted to ground confluence of decreasing systems. Superposition is needed between decreasing conditional rules. As before, we must perform enough expansions with persistent conditional equations for there to always be a normal-form proof in the limit. Decreasing Strategy: An inference sequence Eo 1- E1 1- · · · is fair with respect to the decreasing strategy if where exp(Eoo) is the set of conditional equations that may be inferred from persisting equations by one application of an expansion rule superpose, narrow, or reflect. Theorem 2. If an inference sequence is fair for the decreasing strategy, then for any proof of s ~ t in the initial set Eo of conditional equations, there is a normal­ form proof of 8 ~ t in the limit E 00 · ## 5 Discussion We presented two complete theorem-proving strategies based on the use of term-orderings. Both strategies provide for simplification (demodulation) by what we called "decreasing" equations. Our unit strategy is the first to combine a restriction to paramodulation with unit equations with a strategy based on maximal terms. It limited inferences in the following ways: (1) The functional reflexive axioms are not needed and, at the same time, paramodulation into variables is avoided (as for some versions of paramod­ ulation); (2) for all (resolution and paramodulation) inferences, at least one of the equations must be uncon­ ditional (as in positive unit resolution and positive unit paramodulation); (3) unless an equation is unconditional only its conditional part is used for paramodulation (analogous to positive-unit resolution); (4) only maxi­ mal terms (with respect to a given ordering) are used (analogous to ordered resolution). Unlike [Kounalis and Rusinowitch, 1987], we use only unit clauses when paramodulating into conditions; unlike [Bachmair et a/. , 1989], all inferences use only the maximal side of an equation. The second strategy prefers paramodulation between positive literals. It requires less paramodulation and offers more simplification than [Kounalis and Rusinow­ itch, 1987], for example. In essence, it treats decreasing equations like unit clauses of the first strategy. When the ordering supplied to the prover is empty (the empty ordering is completable), the method reduces to "special" paramodulation, in which the functional­ reflexive axioms are not needed and paramodulation into variables is not performed (see [Lankford, 1975]). The limitations on paramodulation are like those in [Bertling, 1990], but we give a specific, practical strategy for simplification. The strength of these methods, both in minimizing possible inferences and maximizing potential simplifica­ tions, is brought to bear by employing more complete orderings than the empty one. A nonempty ordering eliminates many potential paramodulations and allows conditional equations that are simplifiable to be replaced without compromising (refutation) completeness. In practice, any efficiently computable ordering should be better than uncontrolled paramodulation. The polyno­ mial and path orderings commonly used in rewrite-based theorem provers [Dershowitz, 1987] are completable. In particular, the recursive path orderings have decidability properties [Jouannaud and Okada, 1991] that make it ideal for this purpose. Choosing an ordering that takes the goal (theorem) into account can impart a top-down flavor to an otherwise bottom-up procedure. We used the same ordering for simplification as for choosing the maximal literal. In fact, a different selection strate~y can be used for choosing the literal to narrow, as in lBertling and Ganzinger, 1989], but then the term ordering must be used to choose the larger side of the equality. ## References 1. [Bachmair and Ganzinger, 1990] Leo Bachmair and Harald Ganzinger. Completion of first-order clauses with equality. In M. Okada, editor, Proceedings of the Second International Workshop on Conditional and Typed Rewriting Systems, Montreal, Canada, June 1990. Lecture Notes in Computer Science, Springer, Berlin, to appear. 2. [Bachmair et a/., 1986] Leo Bachmair, Nachum Der- showitz, and Jieh Hsiang. Orderings for equational proofs. In Proceedings of the IEEE Symposium on Log- ic in Computer Science, pages 346-357, Cambridge, MA, June 1986. 3. [Bachmair et a/., 1989] Leo Bachmair, Nachum Der- showitz, and David A. Plaisted . Completion without failure. In H. A•it-Kaci and M. Nivat, editors, Resolu- tion of Equations in Algebraic Structures 2: Rewriting Techniques, chapter 1, pages 1-30. Academic Press, New York, 1989. 4. [Bertling and Ganzinger, 1989] Hubert Bertling and Harald Ganzinger. Completion-time optimization of rewrite-time goal solving. In N. Dershowitz, editor, Proceedings of the Third International Conference on Rewriting Techniques and Applications, pages 45-58, Chapel Hill; NC, April1989. Vol. 355 of Lecture Notes in Computer Science, Springer, Berlin. 5. [Bertling, 1990] Hubert Bertling. Knuth-Bendix com- pletion of Horn clause programs for restricted linear resolution and paramodulation. In S. Kaplan and M. Okada, editors, Extended Abstracts of the Second International Workshop on Conditional and Typed Rewriting Systems, pages 89-95, Montreal, Canada, June 1990. Revised version to appear in Lecture Notes in Computer Science, Springer, Berlin. 6. [Boyer, 1971] Robert S. Boyer. Locking: A restriction of resolution. Ph.d., University of Texas at Austin, Austin, TX, 1971. 7. [Brown, 1975] Thomas Carl Brown, Jr. A Structured Design-Method for Specialized Proof Procedures. PhD thesis, California Institute of Technology, Pasadena, CA, 1975. 8. [Dershowitz and Jouannaud, 1990] Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Hand book of Theoretical Computer Science B: Formal Methods and Semantics, chapter 6, pages 243-320. North-Holland, Amster- dam, 1990. 9. [Dershowitz and Manna, 1979] Nachum Dershowitz and Zohar Manna. Proving termination with multiset orderings. Communications of the ACM, 22(8):465- 476, August 1979. 10. [Dershowitz and Okada, 1988] Nachum Dershowitz and Mitsuhiro Okada. Proof-theoretic techniques and the theory of rewriting. In Proceedings of the Third IEEE Symposium on Logic in Computer Science, pages 104- 111, Edinburgh, Scotland, July 1988. 11. [Dershowitz, 1987] Nachum Dershowitz. Termination of rewriting. J. of Symbolic Computation, 3(1&2):69- 115, February/ April 1987. Corrigendum: 4, 3 (De- cember 1987) , 409-410. 12. [Dershowitz, 1990] Nachum Dershowitz . A maximal- literal unit strategy for Horn clauses. InS. Kaplan and M. Okada, editors, Extended Abstracts of the Second International Workshop on Conditiona l and Typed Rewriting Systems, pages 21-27, Montreal, Canada, June 1990. Concordia University. Revised version to appear in Lecture Notes in Computer Science, Springer, Berlin. [Furbach, 1987] Ulrich Furbach . Oldy but goody: Paramodulation revisited. In Morik, editor, Proceed- ings of the GI Workshop on Artificial Intelligence, pages 195-200, 1987. Vol. 152 of Informatik Fach- berichte. [Ganzinger, 1987] Harald Ganzinger. A completion pro- cedure for conditional equations. In S. Kaplan and J .-P. Jouannaud, editors, Proceedings of the First In- ternational Workshop on Conditional Term Rewriting Systems, pages 62-83, Orsay, France, July 1987 . Vol. 308 of Lecture Notes in Computer Science, Springer, Berlin (1988). 13. [Henschen and Wos, 1974] L. Henschen and L. Wos. U- nit refutations and Horn sets. J. of the Association for Computing Machinery, 21:590-605, 1974. 14. [Hsiang and Rusinowitch, 1986] Jieh Hsiang and Michael Rusinowitch. A new method for establish ing refutational completeness in theorem proving. In J . H. Siekmann, editor, Proceedings of the Eighth International Conference on Automated Deduction, pages 141-152, Oxford, England, July 1986. Vol. 230 of Lecture Notes in Computer Science, Springer, Berlin. [Hsiang and Rusinowitch, 1987] Jieh Hsiang and Michael Rusinowitch. On word problems in equational theories. In T. Ottmann, editor, Proceedings of the Fourteenth EATCS International Conference on Automata, Languages and Programming, pages 54- 71, Karlsruhe, West Germany, July 1987. Vol. 267 of Lecture Notes in Computer Science, Springer, Berlin. 15. [Jouannaud and Okada, 1991] Jean-Pierre Jouannaud and Mitsuhiro Okada. Satisfiability of systems of ordi- nal notations with the subterm property is decidable. In Proceedings of the Eighteenth EATCS Colloquium on Automata, Languages and Programming, Madrid, Spain, July 1991. To appear. 16. [Kaplan, 1987] Stephane Kaplan. Simplifying condition- al term rewriting systems: Unification, termination and confluence. J. Symbolic Computation, 4(3):295- 334, December 1987. 17. [Knuth and Bendix, 1970] Donald E. Knuth and P. B. Bendix. Simple word problems in universal alge- bras. In J . Leech, editor, Computational Problems in Abstract Algebra, pages 263-297. Pergamon Press, Oxford, U. K., 1970. Reprinted in Automation of Reasoning 2, Springer, Berlin, pp. 342-376 (1983). 18. [Kounalis and Rusinowitch, 1987] Emmanuel Kounalis and Michael Rusinowitch. On word problems in Horn theories. In S. Kaplan and J.-P. Jouannaud, editors, Proceedings of the First International Workshop on Conditional Term Rewriting Systems, pages 144-160, Orsay, France, July 1987. Vol. 308 of Lecture Notes in Computer Science, Springer, Berlin (1988). 19. [Lankford, 1975] Dallas S. Lankford. Canonical infer- ence. Memo ATP-32, Automatic Theorem Proving Project, University of Texas, Austin, TX, December 1975. 20. [Nieuwenhuis and Orejas, 1990] Robert Nieuwenhuis and Fernando Orejas. Clausal rewriting. In S. Kaplan and M. Okada, editors, Extended Abstracts of the Second International Workshop on Conditional and Typed Rewriting Systems, pages 81-88, Montreal, Canada, June 1990. Concordia University. Revised version to appear in Lecture Notes in Computer Science, Springer, Berlin. 21. [Paul, 1986] Etienne Paul. On solving the equality prob- lem in theories defined by Horn clauses. Theoretical Computer Science, 44(2):127-153, 1986. 22. [Robinson and Wos, 1969] G. Robinson and L. Wos. Paramodulation and theorem-proving in first order theories with equality. In B. Meltzer and D. Michie, editors, Machine Intelligence ../, pages 135-150. Edin- burgh University Press, Edinburgh, Scotland, 1969. 23. [Rusinowitch, 1989] Michael Rusinowitch. Demonstration Automatique: 124 Automated Reasoning Techniques de rUcriture. InterEditions, Paris, France, 1989. 24. [Zhang and Kapur, 1988] Hantao Zhang and Deepak Kapur. First-order theorem proving using conditional equations. In E. Lusk and R. Overbeek, editors, Proceedings of the Ninth International Conference on Automated Deduction, pages 1-20, Argonne, Illinois, May 1988. Vol. 310 of Lecture Notes in Computer Science, Springer, Berlin.