--- title: "An Equational Approach to Theorem Proving in First-Order Predicate Calculus" authors: - "Deepak Kapur" - "Paliath Narendran" doi: "" url: "https://ijcai.org/proceedings/1985/234" pdf: "https://ijcai.org/proceedings/1985/0234.pdf" venue: "Proceedings of the Ninth International Joint Conference on Artificial Intelligence" year: 1985 pages: "1146-1152" track: "Theorem Proving" keywords: --- # An Equational Approach to Theorem Proving in First-Order Predicate Calculus Deepak Kapur, Paliath Narendran *Proceedings of the Ninth International Joint Conference on Artificial Intelligence*, pages 1146-1152. ## Abstract A new approach for proving theorems in first-order predicate calculus is developed based on term rewriting and polynomial simplification methods . A formula is translated into an equivalent set of formulae expressed in terms of 'true', 'false ', 'exclusive-or', and 'and' by analyzing the semantics of its top-level operator. In this representation, formulae are polynomials over atomic formulae with 'and' as multiplication and 'exclusive-or' as addition, and they can be manipulated just like polynomials using familiar rules of multiplication and addition. Polynomials representing a formula are converted into rewrite rules which are used to simplify polynomials. New rules are generated by overlapping polynomials using a critical-pair completion procedure closely related to the Knuth- Bendix procedure. This process is repeated until a contradiction is reached or it is no Ionger possible to generate new rules. It is shown that resolution is subsumed by this method . ## Full text ## 1. INTRODUCTION A new approach for proving theorems in first-order predicate calculus is presented. The approach is based on term rewriting and polynomial simplification methods, and is simple to understand. A key idea is the observa­ tion that formulae can be viewed as polynomials over atomic formulae when they are expressed solely in terms of boolean connectives 'exclusive-or', 'and' and constants 1 and 0 which stand for truth and falsity, respectively. In straightforward application of the Gröbner basis algo­ rithm developed in (Kandri-Rody and Kapur, 1984). For first-order predicate calculus, additional techniques are developed based on identifying equivalences among for­ mulae using unification. Polynomials are first transformed into rewrite rules and the Gröbner basis is computed by generating critical-pairs among rewrite rules. The critical-pair generation is similar to resolution but is more powerful and allows a Iot more of ßexibility; in fact , it is shown that it subsumes resolution. New poly­ nomials are generated from the critical pairs to augment the basis set of polynomials to obtain a Gröbner basis. If the Gröbner basis consists merely of the rule 1 -+ o then we know that the original formula is unsatisfiable or valid depending upon what we were contradicting. * Partially supported by the National Science Foundation grant MCS-82-11621. This approach is particularly useful for reasoning about domains which can be axiomatized using a finite set of equations. Term rewriting approach for developing decision procedures for equational theories can be in­ tegrated weil with first-order predicate calculus as first­ order predicate calculus itself can be handled using rewrite rules. The proposed approach is motivated by Hsiang's method for theorem proving in first-order predicate cal­ culus based on term rewriting (Hsiang and Dershowitz, 1983) and the approach for generating a Gröbner basis of a polynomial ideal over the integers in (Kandri-Rody and Kapur, 1984). At the theoretical Ievel, the major distinc­ tion between our approach and Hsiang's method is that our method is based on the Grobner basis computation whereas Hsiang's method is based on the extensions of the Knuth and Bendix completion procedure for handling associative and commutative operators developed in (Lankford and Ballantyne, 1977; Peterson and Stickel, 1981). Further, we believe our definitions of unification of monomials, rewriting, Superposition and critical pairs are conceptually simpler to understand than Hsiang's. At the implementation Ievel, our approach seems to be easier to implement than Hsiang's, as it does not need to use associative-commutative unification algorithm or its vari­ ation, called BN-unification by Hsiang, to handle boolean operators. An implementation of our method is under­ way. At this stage, it is difficult to make any comparison between the running times of Hsiang's method and our method; however, initial results seem to suggest that our method is more efficient than Hsiang's. Further, it is too early to say how our method compares with resolution or other theorem proving methods. However, in case of pro­ positional calculus, preliminary experiments suggest that our method is more efficient than the resolution-based LMA theorem prover. In this paper, we give an overview of the approach ex­ hibiting how first-order formulae can be viewed as poly­ nomials and rewrite rules. The method is illustrated us­ ing examples. Further technical details and proofs of the theorems in this paper are given in (Kapur and Naren­ dran, 1984). ## 2. PROPOSITIONAL CALCULUS Given a formula 1 , it is asserted to be 1 or o depend­ ing upon whether 1 is to be shown unsatisfiable or valid, respectively, and it is checked whether a contradiction can be derived. In order to do so, the resulting equation is first translated into an equivalent set of polynomials expressed using 'exclusive-or' (+), 'and' (·), 'true' (1) and 'false' (o). (Since a + a = 0 as weil as a - a = o, we use '+' and '- ' interchangably in the paper; we also often omit '*' among atomic formulae.) This can be done by analyzing the outermost operator of the left-hand-side of the equation; see (Kapur and Narendran, 1984) for de­ tails. In many cases, we may able to generate the con­ tradiction 1 = 0 in the process of obtaining an equivalent set of polynomials, in which case we are done. If not , then the translation gives a set of polynomial equations, say {p, = 0 I 1 ~ i ~ n }. To check whether the polynomial equations Iead to a contradiction or not, we generate its Gröbner basis (Buchberger and Loos, 1982; Kandri-Rody and Kapur , 1984). Informally, a finite set of polynomials constitute a Gröbner basis if and only if evey polynomial has a unique normal form when simplified or reduced using polynomi­ als in the basis. To generate a Gröbner basis, each poly­ nomial equation is converted into a rewrite rufe. This is done by totally ordering atomic formulae which is always possible in the case of propositional calculus. This order­ ing is extended to monomials (products of atomic formu­ lae) based on degree (i.e., size) and lexicographic ordering (cf. Buchherger and Loos, 1982; Kandri-Rody and Kapur , 1984). (In fact any ordering which satisfies the following properties will do: (a) o < 1 < m for any monomial m different from 1 and 0. (b) m 1 < m 2 ~ 8 m 1 < s m 2 for every monomial 8 .) Under a total ordering on monomials, every polynomial has a unique head-monomial, whieh serves as the /eft-hand-side of its rule; the rest of the po­ lynomial serves as the right-hand-side of the rule. W e also include a rule X, 2 -+ X, for eaeh propositional variable X, ( idempotency ru/es) as weil as another rule 2 -+ o. Thus we do not have to deal with any indeter­ minate of degree more than 1 nor do we have to deal with eoeffieients other than 0 or 1. There is also a rule p + o - p , but this is taken eare of automatieally in the Gröbner basis eomputation. The rules thus obtained are used to rewrite polynomials. From these rules, new rules are generated to Iook for a contradietion. For eaeh pair of distinet rules, the overlap of their left-hand-sides is generated by taking the least eommon multiple (lern) of the left-hand-sides. Consider two distinct rules L 1 -+ R 1 and L 2 -+ R 2. Let L be the lern of L 1 and L 2, so L = F 1 L 1 = F 2 L 2· ![Image](https://ijcai.org/proceedings/1985/fulltext/234/image_000000_a3b8a6ff3c7d592ab84dd61241b469dbfcf6c74c6023c4eb1446fae4c980f79f.png) Then < F 1 R 11 F 2 R 2> 1s a critica/ pair generated by the two rules, and F 1 R 1 - F 2 R 2 is its S-polynomial (Bueh­ berger and Loos, 1982; Kandri-Rody and Kapur, 1984). If the two polynomials in a eritieal pair do not reduce to the same normal form (or equivalently, the eorresponding S-polynomial does not reduee to 0), a new rule is added from the normal forms thus obtained. This process is re­ peated anti! no new rules are generated. The resulting basis is a Gröbner basis of the input polynomials. For proofs of eorreetness and termination of this algorithm, see (Kandri-Rody and Kapur, 1984) as this algorithm is a speeial ease of the algorithm for generating the Gröbner basis of an ideal over polynomial rings over the integers. W e would like to point out that in order to deduee a eontradietion from a finite set of polynomials, it is not necessary to eonsider Superpositions with the idempoten­ ey rules; however, these superpositions are needed if a Gröbner basis is to be generated. In many eases, generat­ ing superpositions with idempoteney rules gives rise to simpler rules whieh perform eonsiderable reduetion. EXAMPLE: Consider the problern of ehecking whether the following propositional formula f is unsatisfiable. To prove the formula to be unsatisfiable, we equate f to 1. Using the semanties of 1\ and translating = into +, we obtain the following polynomials: Transforming these into rewrite rules using the ordering x1>x 2>x~>Y1>Y 2>y~ on propositional variables which in­ duees an ordering on products of propositional variables based on size and lexieographic ordering, we get W e eannot use these rules to reduee each other. So, we generate new rules by superposing these rules on each other. Overlapping rules 1 and 2, we obtain a product x 1 x2 x~ on whieh rules 1 and 2 can be applied. ![Image](https://ijcai.org/proceedings/1985/fulltext/234/image_000001_58e21d5a2688eb4fe5a00010d9c587600bd42e2a508ae93886c27283686156bf.png) If we further reduee these polynomials using the above rules, we obtain x~ on one side and Y3 on the other side and all other products cancel with eaeh other. This gives us a new polynomial x ~ + y ~ = 0. The new rule for this polynomial is: 4. x~ -+ Ys· Now rules 3 and 4 give us the contradiction 1 -+ o. There is a mueh simpler way of doing the above ex­ ample by faetoring the above polynomials; see (Kapur and Narendran, 1984) for details. Formulae involving many equivalenee eonneetives are known to often give a Iot of trouble to theorem-provers based on resolution, na­ tural deduction and semantie trees. In the ease of propo­ sitional ealculus, they ean be easily taken care of in our approaeh beeause 'exclusive-or' is one of the main Opera­ tors. ## 2.1 Theoretical Foundations Formulae in polynomial form, as stated above, are ele­ ments of a polynomial ring over a Boolean ring, B = ( {o, 1}, +, * ). Let B [X1, ... ,x.] denote the ring of polynomials over B with the additional property that X, ·X, = X, for each X,. Thus if X" ... , x. are the atomic formulae (propositional variables) in 1 , then 1 is an ele­ ment of B[X1, . .. ,X.]. Theorem 2.1: Let 1 be a propositional formula with propositional variables X 1, ... ,x.. Let I be the set of all polynomials in B [X 1, .. . ,X.l which evaluate to 0 for all assignments of X" ... , x. on which 1 evaluates to 0. Then I is an ideal of B IX ~o ...· x.[. Henceforth we refer to the ideal I mentioned in the above theorem as 'the ideal generated by I '. One way to check whether a formula 1 is valid or unsatisfiable is to analyze the ideal generated by 1 . Theorem 2.2: A propositional formula 1 is valid if and only if the ideal generated by 1 over B[X~o ... ,x.[, where the X, s are propositional variables in 1 , is trivial (i.e., the whole polynomial ring). An analogous theorem for an unsatisfiable formula 1 is that the ideal generating by 1 +1 is trivial. The trivial­ ity of an ideal can be checked by generating its Gröbner basis. If the Gröbner basis of an ideal contains 1, then it is trivial. The method discussed in the previous subsec­ tion for testing validity or unsatisfiability is based on Theorem 2.2 and the Gröbner-basis-based test for triviali­ ty of an ideal. ## 3. FIRST-ORDER PREDICATE CALCULUS The approach discussed in the previous section ex­ tends to first-order predicate calculus. The following ob­ servations are crucial in working out this extension. First­ ly, the atomic formulae in first-order predicate calculus play the roJe of propositional variables. Secondly, quantifiers can be handled by the method of introducing Skolem functions, known as 'Skolemization' (Chang and Lee, 1973). Thirdly, there are in general infinitely many atomic formulae; however unlike in the case of proposi­ tional calculus where propositional variables are indepen­ dent and unrelated to each other, atomic formulae in first-order predicate calculus are related through the mechanism of substitution for variables. In tuitively, this captures the forall rule: [('ilz) A (z )I~ A (t ), where ap­ propriate restrictions are placed on the term t which is substituted for an occurrence of z ( cf. Chang and Lee, 1973). Another technical issue is that in general, it may not be possible to totally order atomic formulae in the case of predicate calculus (again unlike the case of the propositional calculus); by relaxing this requirement , we also allow more flexibility as weil as obtain more general results. The rule corresponding to a polynomial form of a first-order formula thus may have more than one mono­ mial on its left-hand-side. As we show later, if a formula is represented in clausal form (i .e., CNF ), then every poly­ nomial in the set of polynomials equivalent to the formu­ la has a unique head-monomial; furthermore, it is also sufficient to consider those critical pairs which Iead to po­ lynomials with a unique head-monomial. W e first briefly discuss how to handle quan tifiers. If the top-level operator of a formula I = 1 is a Ii quantifier and the associated variable is z, , then remove the quantifier. If the top-level operator is a 3 quantifier and associated variable is z,, then introduce a Skolem func­ tion s, , and replace the occurrences of z, bound to this quantifier by S, (z 1, .. . ,z, ), where z" .. . , x, are the free vari­ ables in 1 . Similarly, we have the dual case for the equa­ tion 1 = o, i.e., we Skolemize ld quantifiers and remove 3 quantifiers. We do not need to bring the formula 1 into prenex normal form first for Skolemization. Instead we Skolemize the quantifiers in place after performing min­ iscoping so that each Skolem function depends upon as few number of free variables as possible (Bledsoe and Ty­ son, 1978). This is done by assigning signs with each of the quantifiers and formulae, and giving rules about how the signs change under various boolean connectives; see (Bledsoe and Tyson, 1978) for details. ## 3.1 DERIVING A CONTRADICTION Assurne that we have obtained a set of polynomials following Skolemization from the original formula without encountering a contradiction; we call this set a basis of the formula. Like in the case of propositional calculus, we generate new polynomials from those in the basis using the method of critical pairs and add them to form a new basis. This completion process (which is relat­ ed to the Knuth-Bendix completion procedure (Knuth and Bendix, 1970)) is continued until it is no Ionger possi­ ble to obtain new rules; In the case of first-order predi­ cate calculus also, we abuse the terminology and call the resulting basis a Gröbner basis. As discussed in (Kapur and Narendran, 1984), the Gröbner basis of a finite set of first-order formulae has the property that every polyno­ mial in their first-order ideal reduces to 0; however, it does not satisfy the other property that every first-order polynomial has a unique normal form with respect to the basis. For propositional calculus, this procedure for gen­ erating a Gröbner basis is guaranteed to terminate. How­ ever, for first-order polynomials, the process of generation of new polynomials may never terminate in some cases. Thus a Gröbner basis in the first-order case may be infinite. The theoretical basis of the Gröbner basis approach for first-order predicate calculus is an extension of the results for propositional calculus discussed in Section 2; for details, see (Kapur and Narendran, 1984). We intro­ duce there the notion of a first-order ring of polynomials which generalizes the concept of a boolean ring of polyno­ mials, the algebraic structure embodying propositional calculus. We also define a first-order ideal to characterize first-order inference in an equational way. This gives us a new way to study first-order predicate calculus in terms of equational logic. We also show in (Kapur and Narendran, 1984) that tile Gröbner basis approach is refutation-complete, or, in other words, if a formula is unsatisfiable, then the Gröbner basis computation will terminate with the rule I -+ 0. ## 3.2 FIRST-ORDER FORMULAE AS REWRITE RULES A first-order polynomial P can be represented as a multiset of monomials (which is a conjunction of atomic formulae) in P; a monomial other than 0 or 1 is assumed not to contain 0 or 1. Let SM(P) denote the multiset of monomials in P. A monomial is represented as a multiset of atomic formulae. 1 Given two first-order polynomials P~o P 2, P 1 is included in P 2, written as P 1 ~ P 2, if and only if SM(Pd is a subset of SM(P2 ). Two monomials M 1 and M 2 are said to be unifiable if and only if there is a substitution u such that u(M d = u(M 2) when considered as multisets. Monomials M 1 and M 2 overlap if and only if there is a substitution u such that u(M I) and u(M 2 ) have a non-trivial greatest common divisor (gcd ); i.e., u unifies at least one atomic formu­ la each from M 1 and M 2 (in other words, the intersection of u(M 1) and u(M 2), viewed as multisets, is non-empty ). 1. Before a polynomial is rewritten using a rule, it is always assumed to be Oat. The result of rewriting however may pro­ duce a polynomial that is not Oat. That is the reason for view­ ing a monomial as a multiset of atomic formulae and a polyno­ mial as a multiset of monomials. 1-lenceforth, Operations U, n, etc., are on multisets. ## 3.2.1 Partial Well-Founded Orderings on Monomials Let < be a well-founded simplification ordering of atomic formulae and terms that is closed under Substitu­ tions. An example of a class of such orderings is the 're­ cursive path ordering' scheme of Dershowitz (Dershowitz, 1982). The ordering < can be extended to a well-founded ordering << on monomials using the multiset ordering given in (Dershowitz, 1982). The ordering << on monomi­ als extends natural!y to a partial ordering on polynomials considered as multisets of monomials. Using the ordering <<. on monomials, we can define head-monomials, denoted by HD(P ), of a polynomial P as the set of maximal monomials in P. In general, HD (P) can have more than one monomial. Let TL (P) = P - HD (P ). Details of an ordering on atomic formulae are discussed in (Kapur and Narendran, 1984). ## 3.2.2 Rewrite Relation The rule corresponding to a polynomial P is HD (P) -+ TL (P ). The rewrite relation -+ induced by a rule is defined as follows: a polynomial Q can be rewrit­ ten using a rule hd -+ tl if and only if there exist a mono­ mial m and substitution 0 such that m · 0 (hd) ~ Q. We replace m * O(hd) by m * D(tl) and get Q' = (Q - m · O(hd)) Um * O(tl) and say that Q -+ Q' by the rule hd -+ t1. As in the case of propositional calculus, the following rules are also used for rewriting in addition to the rules corresponding to polynomials: (B 1) p + 0-+ p, where p is a variable ranging over poly­ nomials; this rule is built into the Gröbner basis compu­ tation. The reflexive, transitive closure of -+ is denoted by .... '. As is usually done in the literature, we often say P reduces to Q if P .... ' Q . It should not be hard to see that for any finite set R of polynomials, the rewrite rela­ tion induced by R is Noetherian (i.e. the rewriting process terminates). ## 3.3 CRITICAL PAIRS AND GROBNER BASIS COMPUTATION To check for contradiction, we generate new rules by superposing the existing rules in a given basis. We fi.rst consider a simple case; later we consider a more general case. I. Given two rules (not necessarily distinct) m a basis, where hd 1 and hd 2 are monomials, if hd 1 and hd 2 overlap, then a Superposition P is constructed as fol­ lows: Let u be a most general unifi.er unifying G 1 and G 2, where G, is a subset of hd,, i= 1,2. Let o{G 1) = u(G2) = G, say, and G, f, = hd, , i = 1,2. For each such G 1o G 2, and u, P = u(f t) G o{J 2) = u(hdt} o{J 2) = o{hd 2) u(f t) Then a critical pair is obtained by rewriting P in two different ways: Now, we generalize the above construction to the case when the left-hand-sides of rules are not necessarily single monomials. W e have: hd 1 =h,,+h, 2 + ··· +h,,, and hd2 =h 11 +h 12 + ··· +h 1 · a superposition P is constructed as follows: If :3 u , v : h,, = f 1 G 1 and h 1 , = f 2 G 2 ( G 1 and G 2 could be 1 ), such that G 1 and G 2 can be unifi.ed by a most gen­ eral unifi.er u, i.e., u(G 1)=o{G2)= G, say, then for each such u , v , G 11 G2, and u, we have m1 = u(f 2), m2 = o{J t) and Note that m 1 u(h,.) = o{J tf 2) o{G) = m 2 o{h 1 ,). We ·have: Thus a critical pair for the above two rules is · t <m 1o{ll 1) + m2E o{h 1 ,), m1 E o{h,,) + m2u(112)> . t:::::~~:l sz:zl t"<v s"<u If a critical pair <c~> c2> is trivial, i.e., the S­ polynomial c 1 + c 2 reduces to o, then it is discarded; oth­ erwise, the basis is augmented by adding the rule corresponding to anormal form of c 1 - c 2 · Note that in general there could be many critical pairs generated by two rules as, fi.rstly, the left-hand-sides of rules are polynomials instead of monomials, and secondly, a monomial could overlap with another monomial in more than one way. And, a rule can overlap with itself and generate a new rule in the fi.rst-order case, whereas that does not happen in propositional calculus. It should be easy to see that the rules (8 1), (8 2) and (B!) by themselves do not generate any new rules. How­ ever, these rules (especially the idempotency rule (8 2 ) and the "self-inverse" rule (B !)) can interact with rules in a basis of a fi.rst-order formula to generate new rules; the critical pairs among them are defi.ned below. II. Given a rule hd -+ II, where hd = h 1 + · · · + h, , and an idempotent rule of the form P(xl>···· x.)*P(x 1, ··· ,x.)-+P(x1, ·.· ,x. ), suchthat the predicate P is used in some h, , the following two cases can arise: (a) There is a superposition of the two rules: Iet u be a substitution which unifies P (x 1, ·.· , x.) and the atomic for­ mula P ( 1 I> . ·· , 1.) in lt" then the Superposition s is o{P(x 1, ... ,x.)ht) + ··· +o{P(xl>···· x.)ht}, where u = { x 1 +- I 1o ··· , x. +- 1. } , and the critical pair < c ~> c 2> is obtained from S by respectively applying the two rules. (b) For the above two rules, i.e., hd ..... II and P(xl>····x.)*P(xl>····x.)-+P(x 1, ··· ,x.), there is yet another way of generating a Superposition. If h, contains two dis­ tinct occurrences of the predicate symbol P, say P (t 1, ... , 1.) and P (s ~> ... , s. ), and u is a most general sub­ stitution which unifies these atomic formulae, then a Su­ perposition is obtained by applying u on hd and a critical pair is obtained by applying the above two rules to the superposed term. III. The interaction between the self-inverse rule 1 + 1 -+ o and a rule hd -+ II in a basis results in new rules as fol­ lows: If hd contains h, and h 1 which can be unified, i.e., there is a most general substitution u so that o{h,) = o{h 1 ) , then the Superposition is obtained by applying u on hd and a critical pair is obtained by applying the two rules to it . These Superpositions need to be considered only for rules having many monomials on their left-hand-sides. ## 3.4 GROBNER BASIS The above process of generating critical pairs is re­ peated until the contradiction 1 = o is generated or it is no Ionger possible to generate any new rule. In the first case, we are done; in the second case, the original formula is falsified (respectively, satisfiable) if it is being proved valid (respectively, unsatisfiable). The Gröbner basis thus obtained provides a way to construct a model for falsifiability (satisfiability) of the formula as an example in the next section illustrates. As stated earlier, the pro­ cess of generating critical pairs could continue forever for formulae which arenot valid (respectively, unsatisfiable). ## 4. EXAMPLES Consider a simple formula: All unicorns are qua­ drupeds and there is a quadruped imply that there is a unicorn. If U stands for something being a unicorn and Q stands for something being a quadruped, then this formu­ la is: To show the validity of the above formula, we equate it to 0, we obtain After Skolemization, we have: Because of U (z) = o, the first equation becomes redun­ dant. Polynomials Q (a)-+ 1 and U(z)-+ 0 do not gen­ erate any additional rules thus giving us a Gröbner basis. So, the original formula is not valid because we did not derive a contradiction. The original formula is falsified in a I-element model in which U(a) = 0 and Q (a) = 1. The following example is taken from (Chang and Lee, Hl73). Consider a formula which states that (i) if there exists an element such that it is the left-identity as weil as the right-identity of every element and that for every element z , i (z) serves as the left-inverse as weil as right­ inverse of z, and (ii) if whenever z and 11 are in a subset P , then so is z operated with i (II ), then the subset P is closed under the function i. To prove this formula to be a theorem, we assert it to 0 and deduce a contradiction. Translating the assertion to equivalent set of polynomials gives us the following rewrite rules: the constant symbols e and b are the Skolem functions introduced to get rid of quantifiers. Variables in each rule are standardized apart. From rules 6 and 7, we get a critical pair by substitu ting i ( b ) for z; ![Image](https://ijcai.org/proceedings/1985/fulltext/234/image_000002_f337649e9ca40186e1056193b88ec222228b121c52a1811e1438251443cde9ad.png) Let us Iabel the new rule as 8, i.e., 8. P ( z ) P (II ) M ( z , i (II ), i ( b )) -+ 0. Similarly, a critical pair between rules 1 and 8 using the substitution { z - e , 11 - b }, after normalization, is, Using rules 5 and 10, we get the contradiction which im­ plies that the original formula we started with is valid. ## 6. RELATING RESOLUTION TO THE GROBNER BASIS APPROACH The process of generating critical pairs of first-order polynomials is similar to resolving the corresponding for­ mulae. Below, we show that resolution can be simulated by the critical-pair-generation process. In fact , for certain formulae for which resolution does not give any meaning­ ful result, computing critical pairs of the corresponding polynomials may still produce useful inferences. Theorem 6.1: Let 8 1 = C1 V I 1(C2, .. . , Gm ), and t 1 = ~ C; \1 I .J..D 2, .. . , D.) be two clauses ( disjunction of literals), where C, , 1 ~ i ~ m, c; , and D 1 , 2 ~ j ~ n , are positive literals. Let their binary resolvent on c 1 be u 1 = 11(1 1( C 2 ... ..Cm )) \1 utl .J..D 2, . .. ,D. )), where 11 is the most generat unifier of C 1 and C; . Then a polynomial form of u 1 + 1 can be obtained from an S-polynomial of the poly­ nomial forms of 8 1 + 1 and t 1 + 1. Theorem 6.2: Let 8 be a clause and 11 be a most general unifier of two literals in 8 of the same sign. Then a polynomial form of u(a) + 1 can be obtained from an S­ polynomial of the polynomial form of a + 1 and the rule (82)· Theorem 5.2 shows that the process of computing factors of clauses ( cf. Chang and Lee, Hl73, p. 80), which is part ## 1. REFERENCES - 111 Bledsoe, W. W., and Tyson, M. "The UT Interactive Prover," Automatie Theorem Proving Project, ATP-17A, Department of Mathematics and Computer Sciences, University of Texas, Austin, June, 1978. - 12] Buchberger, B., and Loos, R. "Algebraic Simplification" In Computer Algebr11: Svmbolic 11nd Algebr11ic Comput11tion (Eds. B. Buchberger, G.E. Collins and R. Loos), Computing Suppl. 4, Springer Verlag, New York, 1982, pp. 11-43. - 13] Chang, C-L. and Lee, R.C. Svmbolic Logic 11nd Mecllllniclll Theorem Proving. Academic Press, New York, 1973. - 14] Dershowitz, N. "Orderings for Term Rewriting Systems." Tlleoretical Computer Science 17 (1982), pp. 279-301. - I5J Hsiang, J. and Dershowitz, N. "Rewrite Methods for Clausal and Non-clausal Theorem Proving" In Proc. 10th EATCS Intl. Colloq. on Autom11t11, L11ngu11gea, ond Progr11mming, Spain, 1983. - 16] Kandri-Rody, A., and Kapur, D. "Computing the Gröbner Basis or a Polynomial Ideal over Jntegers" In Proc. Tllird MACSYMA Uaera ' Conference, Schenectady, NY, July 1984, pp. 436-451. of the resolution method, can be simulated by repeated overlapping of polynomial rules with the rule (8 2). Thus resolution is built into the critical pair generation process as each of the four cases in the definition of aresolvent in (er. Chang and Lee, 1973, pp. 80-81), can be simulated . - 17] Kapur, D., and Narendran, P. "An Equational Approach to Theorem Proving in First-Order Predicate Calculus," 84CRD296, General Electric Corporate Research and Develop­ ment Report, Schenectady, NY, March, 1984; Revised, Dec. , 1984. - 18] Knuth, D.E. and Bendix, P .B. "Simple Word Problems in Universal Algebras" In Comput11tionol Problems in Abatr11ct Algebroa. (Ed. J. Leech), Pergarnon Press, 1970, pp. 263-297. - 19] Lankford, D.S., and Ballantyne, A.M., "Decision Procedures for Simple Equational Theories with Commutative-Associative Axioms: Complete Sets or Commutative-Associative Reduc­ tions," Automatie Theorem Proving Project, Dept. of Math. and Computer Science, University of Texas, Austin, TX 78712, Report ATP-39, August 1977. - 110] Peterson, G.L., and Stickel, M.E., "Complete Sets of Reduc­ tions for Some Equational Theories," JACM 28 (1981), pp. 233-264. - 111] Robinson, J. A. "A Machine-Oriented Logic Based on the Resolution Principle." JACM 12 (1965), pp. 23-41. - 112] Slagle, J. R. "Automated Theorem Proving for Theories with Simplifiers, Commutativity and Associativity." JACM 21 (1974), pp. 622-642. - 113] van der Waerden, B.L., Modern Algebr11. Vols. I and II, Fredrick Ungar Publishing Co., New York, 1966. ## References 1. Bledsoe, W. W., and Tyson, M. "The UT Interactive Prover," Automatie Theorem Proving Project, ATP-17A, Department of Mathematics and Computer Sciences, University of Texas, Austin, June, 1978. 2. Buchberger, B., and Loos, R. "Algebraic Simplification" In Computer Algebr11: Svmbolic 11nd Algebr11ic Comput11tion (Eds. B. Buchberger, G.E. Collins and R. Loos), Computing Suppl. 4, Springer Verlag, New York, 1982, pp. 11-43. 3. Chang, C-L. and Lee, R.C. Svmbolic Logic 11nd Mecllllniclll Theorem Proving. Academic Press, New York , 1973. 4. Dershowitz, N. "Orderings for Term Rewriting Systems." Tlleoretical Computer Science 17 (1982), pp. 279-301. 5. I5J Hsiang, J. and Dershowitz, N. "Rewrite Methods for Clausal and Non-clausal Theorem Proving" In Proc. 10th EATCS Intl. Colloq. on Autom11t11, L11ngu11gea, ond Progr11mming, Spain, 1983. 6. Kandri-Rody, A., and Kapur, D. "Computing the Gröbner Basis or a Polynomial Ideal over Jntegers" In Proc. Tllird MACSYMA Uaera ' Conference, Schenectady, NY, July 1984, pp. 436-451. 7. Kapur, D., and Narendran, P. "An Equational Approach to Theorem Proving in First-Order Predicate Calculus," 84CRD296, General Electric Corporate Research and Develop- ment Report, Schenectady, NY, March, 1984; Revised, Dec., 1984. 8. Knuth, D.E. and Bendix, P .B. "Simple Word Problems in Universal Algebras" In Comput11tionol Problems in Abatr11ct Algebroa. (Ed. J. Leech), Pergarnon Press, 1970, pp . 263-297. 9. Lankford, D.S., and Ballantyne, A.M., "Decision Procedures for Simple Equational Theories with Commutative-Associative Axioms: Complete Sets or Commutative-Associative Reduc- tions," Automatie Theorem Proving Project, Dept. of Math. and Computer Science, University of Texas, Austin, TX 78712, Report ATP-39, August 1977. 110 10. Peterson, G.L., and Stickel, M.E., "Complete Sets of Reduc- tions for Some Equational Theories," JACM 28 (1981), pp. 233-264 . 111 11. Robinson , J. A. "A Machine-Oriented Logic Based on the Resolution Principle." JACM 12 (1965), pp. 23-41. 112 12. Slagle, J. R. "Automated Theorem Proving for Theories with Simplifiers, Commutativity and Associativity ." JACM 21 (1974), pp. 622-642. 113 13. van der Waerden, B.L., Modern Algebr11. Vols. I and II, Fredrick Ungar Publishing Co., New York , 1966.