Rewrite Techniques in Theorem Proving

Leo Bachmair Harald Ganzinger

Tutorial—CADE’94

1 Introduction

Rewrite techniques, as exemplified by completion procedures, have been successfully applied to many problems in equational theorem proving. The theoretical foundation of completion is the use of rewrite rules, guided by well-founded syntactic orderings, in such a way that certain commutation properties are satisfied. From a practical point of view the simplification techniques afforded by rewriting are also important. In the context of automated theorem proving, rewrite techniques have been typically applied to equivalence relations. Recently it has been shown how to extend these methods to arbitrary transitive relations. This tutorial gives an introduction into fundamental techniques of automated first-order theorem proving from the perspective of rewriting.

2 Overview

The tutorial consists of three parts, each of which is centered around a basic concept or technique of rewriting.

2.1 Orderings

In the first part we introduce orderings as a means to restrict the search space of deductive inference systems. Orderings can be used to specify certain minimal models (called perfect models in logic programming) and to refine inference rules so that they essentially approximate computation in this distinguished model. We discuss ordered resolution as one example. Selection for negative literals (like in SLD-resolution) will be introduced as a means to exploit forms of “don’t care non-deterministism” within the deductive process. We present a general completeness result for a resolution scheme which is parameterized by the two parameters of an ordering and a selection function. As examples of two (quite different) instances of this resolution scheme we will explain hyperresolution and lock resolution.

2.2 Chaining

Ordered resolution with selection may be viewed as an efficient rewriting technique for the transitive relation “implication” (in the presence of additional algebraic structure for conjunction and disjunction). The second part of the tutorial is devoted to rewrite techniques for transitive relations in general. For logical theories with transitive relations, such as logics with equality or inequality relations, the various refinements of resolution are not very effective. Special techniques have been devised for such theories: chaining and variable elimination for inequalities, and paramodulation, which can be thought of as a form of subterm chaining, for equality. Chaining essentially encodes certain resolution steps with the transitivity axiom. For example, if < is a transitive relation, chaining allows one to derive uσ < vσ from u < s and t < v, where σ is a most general unifier of s and t. We consider the following refinement of chaining: first compare the term sσ (which is identical to tσ) to both uσ and vσ (using a given well-founded ordering on terms) and perform the chaining inference only if sσ is maximal. This form of “ordered chaining” can be viewed as an application of standard rewrite techniques. More precisely, it corresponds to a completion process, aimed at deriving enough rewrite rules so that the given transitive relation can be described by corresponding rewrite proofs. The completeness of ordered chaining is based on a suitable commutation property of the rewrite relations involved which is achieved through completion.

We will present chaining-based inference systems for Horn clauses and general clauses, respectively. In addition, a general notion of redundancy is provided by which the compatibility of simplification techniques with any instance of that scheme can be separately investigated. We will explain why the inference systems are refutationally complete and compatible with the deletion of redundant clauses and inferences. Moreover we will see how to extend the concept of ordered chaining to almost arbitrary families of composition laws for binary relations.

We will also explain modifications and improvements to these systems that can be made in the presence of additional logical properties such as symmetry, monotonicity or totality — equality and total orderings being especially important applications. For instance, the practicality of chaining methods crucially depends on the extent to which a particularly prolific form of chaining, called variable chaining (where s or t is a variable), can be restricted. Ordered chaining considerably cuts down the number of possible variable chainings, as the required maximality condition for terms can only be satisfied if the variable is unshielded, i.e., occurs only as an argument of the predicate <, but not as an argument of a function symbol or any other predicate symbol. However, we also demonstrate that some variable chainings are needed for transitive relations in general, though further restriction are possible if additional properties such as symmetry are satisfied. For instance, in the case of equivalence relations we obtain calculi in which chaining “into” a variable is not needed.

2.3 Redundancy

In the third part we continue the exploration of chaining for the special case of equality relations. We present superposition as a basic inference and describe corresponding notions of redundancy. We will give an overview of several simplification techniques that have been proved effective in practice.

We then step back again and characterize redundancy in more abstract terms, introducing the notion of a redundancy criterion. We analyse the notion of saturation of a set of clauses up to redundancy. Such saturated sets have the nice property of having a model, unless the empty clause is present. In other words, their satisfiablity is decidable. We derive sufficient, so-called fairness conditions on the strategy employed by a prover, so that correctness is ensured in the sense that a saturated set of clauses is obtained by any fair strategy. As a final illustration of redundancy, we discuss why chaining at or below variables can be avoided for certain theories (e.g., equality or dense, total orderings with no endpoints).

3 Annotated Bibliography

The following bibliography contains items that are directly related to the material discussed in the tutorial. It does not cover all the work on rewrite techniques in theorem proving, but additional references may be found in the proceedings of the conferences on Rewriting Techniques and Applications (all published in Lecture Notes in Computer Science) and in surveys on rewriting (e.g., Dershowitz and Jouannaud 1990), on theorem proving (e.g., Plaisted 1990), and on resolution (Fermüller, Leitsch, Tammet, et al. 1993).

3.1 Equational Reasoning

Rewrite-based techniques to automated theorem proving have their origin in the completion procedure by Knuth and Bendix (1970) which attempts to construct a convergent rewrite system from a given set of universally quantified equational axioms. A convergent rewrite system provides a decision procedure for the underlying equational theory. The completion procedure may fail to find a convergent system, but has been extended to a refutationally complete theorem prover (cf. Lankford (1975), Hsiang and Rusinowitch (1987), Bachmair, Dershowitz and Plaisted (1989)).

Paramodulation was introduced by Robinson and Wos (1969), but all early completeness proofs assumed the presence of “functional-reflexive axioms” and required paramodulation into variables (i.e., chaining into variables). Brand (1975) was the first to prove that the functional-reflexive axioms are not needed, and his proof requires only a very limited form of paramodulation into a variable. The first proof that paramodulation into a variable is not needed at all was given by Peterson (1983), while Hsiang and Rusinowitch (1991) were the first to explicitly put some ordering restrictions on paramodulation. The more restrictive superposition calculus described in Zhang and Kapur (1988), Zhang (1988) turns out to be incomplete; for a counterexample see Bachmair and Ganzinger (1990). The superposition calculus with equality factoring was introduced by Bachmair and Ganzinger (1990). There are also alternatives to equality factoring: Rusinowitch (1991) weakens some ordering constraints, while merging paramodulation is proposed in Bachmair and Ganzinger (1990), see also Pais and Peterson (1991). Basic paramodulation and superposition calculi have been proposed by Bachmair, Ganzinger, Lynch, et al. (1992) and Nieuwenhuis and Rubio (1992). Recent advances in this area are described by Nieuwenhuis and Rubio (1994) (also see Vigneron 1994) and Marché (1994).

3.2 Chaining

Slagle (1972) was the first to propose a chaining system with paramodulation for theories with equality, orderings and sets. The functional reflexive axioms and paramodulation into variables were required. Bledsoe and Hines (1980) have investigated dense total orderings without endpoints and have developed techniques for eliminating certain occurrences of variables from formulas. In their inference system, no chaining through variables is performed and no explicit inferences with transitivity, density, totality and the “no endpoints” axioms are computed. Completeness results for particular such systems of restricted chaining are proved by Bledsoe, Kunen and Shostak (1985) and Hines (1992). Theorem provers developed from these theoretical investigations have performed successfully in proving theorems such as the continuity of the sum of two continuous functions or the intermediate value theorem; see Bledsoe and Hines (1980), Hines (1988) or Hines (1990). These calculi lack an efficient treatment of equality as an equality s ≈ t is represented by two inequalities s ≤ t and t ≤ s. The disadvantage of this approach is that the implicitly specified equality relation requires additional congruence axioms for each function symbol, while such powerful simplification mechanisms as demodulation cannot be used. Subterm chaining methods for general clauses in the presence of (anti-) monotonicity have been proposed by Manna and Waldinger (1986), but for completeness chaining into the variables of functional-reflexive axioms (cf. the “variable instance pairs” in Bachmair, Dershowitz and Hsiang 1986) is required (Manna and Waldinger 1992) which is impractical in general.

Levy and Agustí (1993) were the first to apply the concept of commutation to non-symmetric (monotone) relations. They have described a completion procedure for unit inequations and have investigated the problem of chaining into variables for distributive lattices. Bachmair and Ganzinger (1993b) have given a refutationally complete inference system of ordered chaining for general clauses and general transitive relations. It was shown how to specialize the system in the presence of additional logical properties such as symmetry, monotonicity and reflexivity. In particular, (partial) equivalence and congruence relations were discussed. The inference systems were shown to be compatible with a general notion of redundancy by which the usual simplification and deletion techniques were covered. The particular case of total orderings was studied in (Bachmair and Ganzinger 1993a) where a “maximal” variant of ordered chaining was proposed to deal with disjunctions. Compatibility of this inference system with redundancy allowed to show that the variable elimination techniques for dense total orderings without endpoint are admissible simplifications. Hence, ordered chaining through variables is not needed in that case. The latter paper also shows, by giving an ordered chaining system for theories with equality and total orderings, how to combine superposition with chaining and how to obtain ordered chaining systems for “arbitrary” families of composition laws for binary relations.

References

L. Bachmair, N. Dershowitz and J. Hsiang, 1986. Orderings for equational proofs. In Proc. Symp. Logic in Computer Science, pp. 346–357, Boston, Massachusetts.

L. Bachmair, N. Dershowitz and D. Plaisted, 1989. Completion without failure. In H. Ait-Kaci, M. Nivat, editors, Resolution of Equations in Algebraic Structures, vol. 2, pp. 1–30. Academic Press.

L. Bachmair and H. Ganzinger, 1990. On Restrictions of Ordered Paramodulation with Simplification. In M. Stickel, editor, Proc. 10th Int. Conf. on Automated Deduction, Kaiserslautern, Lecture Notes in Computer Science, vol. 449, pp. 427–441, Berlin, Springer-Verlag.

L. Bachmair and H. Ganzinger, 1993. Ordered Chaining for Total Orderings. Technical Report MPI-I-93-250, Max-Planck-Institut für Informatik, Saarbrücken. Short version to appear in Proc. CADE’94.

L. Bachmair and H. Ganzinger, 1993. Rewrite Techniques for Transitive Relations. Technical Report MPI-I-93-249, Max-Planck-Institut für Informatik, Saarbrücken. Short version to appear in Proc. LICS’94.

L. Bachmair, H. Ganzinger, Chr. Lynch and W. Snyder, 1992. Basic Paramodulation and Superposition. In D. Kapur, editor, Automated Deduction — CADE’11, Lecture Notes in Computer Science, vol. 607, pp. 462–476, Berlin, Springer-Verlag.

W. Bledsoe, K. Kunen and R. Shostak, 1985. Completeness results for inequality provers. Artificial Intelligence, Vol. 27, pp. 255–288.

W. W. Bledsoe and L. M. Hines, 1980. Variable Elimination and Chaining in a Resolution-based Prover for Inequalities. In Wolfgang Bibel, Robert Kowalski, editors, 5th Conference on Automated Deduction, LNCS 87, pp. 70–87, Les Arcs, France, Springer-Verlag.

D. Brand, 1975. Proving theorems with the modification method. SIAM Journal of Computing, Vol. 4, pp. 412–430.

N. Dershowitz and J.-P. Jouannaud, 1990. Rewrite Systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science B: Formal Methods and Semantics, chapter 6, pp. 243–309. North-Holland, Amsterdam.

C. Fermüller, A. Leitsch, T. Tammet and N. Zamov, 1993. Resolution Methods for the Decision Problem (LNAI 679). Springer-Verlag.

L. Hines, 1990. Str+^{.}ve⊆: The Str+^{.}ve-based Subset Prover. In Mark E. Stickel, editor, 10th International Conference on Automated Deduction, LNAI 449, pp. 193–206, Kaiserslautern, FRG, Springer-Verlag.

L. M. Hines, 1992. Completeness of a Prover for Dense Linear Logics. Journal of Automated Reasoning, Vol. 8, pp. 45–75.

L.M. Hines, 1988. Hyper-chaining and knowledge-based theorem proving. In Proc. 9th Int. Conf. on Automated Deduction, Lecture Notes in Computer Science, pp. 469–486. Springer-Verlag.

J. Hsiang and M. Rusinowitch, 1991. Proving refutational completeness of theorem proving strategies: The transfinite semantic Tree method. Journal of the ACM, Vol. 38, No. 3, pp. 559–587.

Jieh Hsiang and Michael Rusinowitch, 1987. On Word Problems in Equational Theories. In Proc. 14th ICALP, Lecture Notes in Computer Science, vol. 267, pp. 54–71, Berlin, Springer-Verlag.

D. Knuth and P. Bendix, 1970. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pp. 263–297. Pergamon Press, Oxford.

D. Lankford, 1975. Canonical inference. Technical Report ATP-32, Dept. of Mathematics and Computer Science, University of Texas, Austin.

J. Levy and J. Agustí, 1993. Bi-rewriting, a Term Rewriting Technique for Monotonic Order Relations. In C. Kirchner, editor, Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol. 690, pp. 17–31, Berlin, Springer.

Z. Manna and R. Waldinger, 1986. Special Relations in Automated Deduction. Journal of the ACM, Vol. 33, pp. 1–60.

Z. Manna and R. Waldinger, 1992. The Special-Relation Rules are Incomplete. In Deepak Kapur, editor, 11th International Conference on Automated Deduction, pp. 492–506, Saratoga Springs, NY, Springer LNAI 607.

C. Marché, 1994. Normalized rewriting and normalized completion. In Proc. 9th IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press.

R. Nieuwenhuis and A. Rubio, 1992. Basic superposition is complete. In ESOP’92, Lecture Notes in Computer Science, vol. 582, pp. 371–389, Berlin, Springer-Verlag.

R. Nieuwenhuis and A. Rubio, 1994. AC-superposition with constraints: No AC-unifiers needed. In Proc. 12th International Conference on Automated Deduction, Lecture Notes in Computer Science, Berlin, Springer-Verlag.

John Pais and G.E. Peterson, 1991. Using Forcing to Prove Completeness of Resolution and Paramodulation. Journal of Symbolic Computation, Vol. 11, pp. 3–19.

Gerald E. Peterson, 1983. A technique for establishing completeness results in theorem proving with equality. SIAM J. on Computing, Vol. 12, No. 1, pp. 82–100.

D. A. Plaisted, 1990. Mechanical theorem proving. In R. B. Banerji, editor, Formal Techniques in Artificial Intelligence. Elsevier.

G.A. Robinson and L. T. Wos, 1969. Paramodulation and theorem proving in first order theories with equality. In B. Meltzer, D. Michie, editors, Machine Intelligence 4, pp. 133–150. American Elsevier, New York.

M. Rusinowitch, 1991. Theorem proving with resolution and superposition: An extension of the Knuth and Bendix completion procedure as a complete set of inference rules. J. Symbolic Computation, Vol. 11, pp. 21–49.

J. R. Slagle, 1972. Automatic theorem proving for theories with Built-in Theories Including Equality, Partial Orderings, and Sets. Journal of the ACM, Vol. 19, pp. 120–135.

L. Vigneron, 1994. Associative-commutative dedution with constraints. In Proc. 12th International Conference on Automated Deduction, Lecture Notes in Computer Science, page ??, Berlin, Springer-Verlag.

H. Zhang, 1988. Reduction, superposition and induction: Automated reasoning in an equational logic. PhD thesis, Rensselaer Polytechnic Institute, Schenectady, New York.

H. Zhang and D. Kapur, 1988. First-order theorem proving using conditional rewrite rules. In E. Lusk, R. Overbeek, editors, Proc. 9th Int. Conf. on Automated Deduction, Lecture Notes in Computer Science, vol. 310, pp. 1–20, Berlin, Springer-Verlag.