Equational inference, canonical proofs, and proof orderings

ABSTRACT

We describe the application of proof orderings—a technique for reasoning about inference systems-to various rewrite-based theorem-proving methods, including refinements of the standard Knuth-Bendix completion procedure based on critical pair criteria; Huet's procedure for rewriting modulo a congruence; ordered completion (a refutationally complete extension of standard completion); and a proof by consistency procedure for proving inductive theorems.

REFERENCES

• 1: Siva Anantharaman , Jieh Hsiang, Automated proofs of the Moufang identities in alternatives rings, Journal of Automated Reasoning, v.6 n.1, p.79-109, Mar. 1990 [doi>10.1007/BF00302643]
• 2: ~B,\CItMAIR, L., 1991. Proof methods for equational theories. Ph.D. dissertation. Univ. Illinois, ~Urbana-Champalgn, Ill., 1987. (A revised version, titled Canonical Equational Proofs, has been ~published by Birkhiiu~er, Boston, 1991.)
• 3: ~BACHMAtR, m., AND DERSHOWITZ, N., 1987. Inference rules for rewrite-based first-order theo- ~rem proving. In Proceedings of the 211d Symposium on Logic in Computer Science, (Ithaca, N.Y., ~June). New York, IEEE, pp. 331-337.
• 4: L. Bachmair , Nachum Dershowitz, Critical pair criteria for completion, Journal of Symbolic Computation, v.6 n.1, p.1-18, August 1988 [doi>10.1016/S0747-7171(88)80018-X]
• 5: L. Bachmair , Nachum Dershowitz, Completion for rewriting modulo a congruence, Theoretical Computer Science, v.67 n.2-3, p.173-201, Oct. 1989 [doi>10.1016/0304-3975(89)90003-0]
• 6: ~BACHMAm, L., DERSHOWITZ, N., AND PLAISTED, D.A., 1989. Completion without failure. In ~ Resolution oj Equatzon~ in Algebraw Structures 2: Rewnnng Techniques, chapter 1. H. A'it-Kaci ~and M. NJvat, eds. Academic Press, Orlando, Fla., pp. 1-30.
• 7: Leo Bachmair , Harald Ganzinger, On restrictions of ordered paramodulation with simplification, Proceedings of the tenth international conference on Automated deduction, p.427-441, July 1990, Kaiserslautern, Germany
• 8: ~BACHMAIR, L., ,\ND GANZINGER, H., 1991. Rewrite-based equational theorem proving with ~selection and simplification. Tech. Rep, MP1-I-91-208. Max-Planckdnsntut fur Informank, ~Saarbriicken, Germany, 1991. To appear in J. Logtc Computat.
• 9: Leo Bachmair , Harald Ganzinger, Non-Clausal Resolution and Superposition with Selection and Redundancy Criteria, Proceedings of the International Conference on Logic Programming and Automated Reasoning, p.273-284, July 15-20, 1992
• 10: H. Bertling , H. Ganzinger, Completion-time optimization of rewrite-time goal solving, Proceedings of the 3rd international conference on Rewriting Techniques and Applications, p.45-58, January 1989
• 11: ~BOUDET, A., JOUANNAUD, J.-P., AND SCHMIDT-Sc'HAUf3, M., 1988. Unification in free extensions ~of Boolean rings and Abehan groups. In Proceedings of the 3rd Annual Symposium on Logtc m ~Computer Science, (Edinburgh, Scotland), IEEE, New York, pp. 121 130.
• 12: ~BROWN, T. C., JR., 1975. A structured design-method for specialized proof procedures. Ph.D. ~dissertation. California Inst. Tech., Pasadena, CA.
• 13: Bruno Buchberger, A critical-pair/completion algorithm for finitely generated ideals in rings, Proceedings of the Symposium "Rekursive Kombinatorik" on Logic and Machines: Decision Problems and Complexity, p.137-161, May 23-28, 1983
• 14: R. Bündgen , W. Küchlin, Computing ground reducibility and inductively complete positions, Proceedings of the 3rd international conference on Rewriting Techniques and Applications, p.59-75, January 1989
• 15: ~BUTLER, G., AND LANKkORD, D. S., 1980. Experiments with computer implementations of ~procedures which often derive decision algorithms for the word problem in abstract algebras. ~Memo MTP-7, Department of Mathematics, Louisiana Tech. Umversity, Ruston, La. August.
• 16: ~COMON, H., 1990. Solwng incquations in term algrebas. In Proceedinga of the 5tt: Annual ~ ~%~,tnpo~tttm on Logic In Computer Science, (Phdadelphia, Pa.). IEEE, New York, pp. 62-69.
• 17: ~DERSHOWn'Z, N., 1982. Applications of the Knuth-Bendix completion procedure. In Proceed- ~ rags' of the Semmatre d'hlformattque Ttzeonque, (Paris, France). Dec.
• 18: Nachum Dershowitz, Termination of rewriting, Journal of Symbolic Computation, v.3 n.1-2, p.69-116, Feb./April 1987 [doi>10.1016/S0747-7171(87)80022-6]
• 19: ~DERsnowrrz, N., 1089. Completion and its applications. In Resohttton ofEquatzonsm Algebn~tc ~Strttctttl'e.$' 2' Rewriting Tectmtques, chapter 2, H. Alt-Kact and M. Nivat, cds. Acadennc Press, ~Orlando, Fla., pp. 31 86.
• 20: ~DLRSHOWFrZ, N, 1991. Ordering-based strategies for Horn clauses. In Proceedings of the }2th ~hlternattonal Joint Conference on Arttfictal lnte{{tgence (Sydney, Australia) Aug., pp. 118-124.
• 21: ~DLRS}K)WITZ, N., 1992. Rewriting methods for word problems. In M. Ito, ed., Words, Lan- ~,k, tttt~,t~,~ cq, CortltIJl'tzatot{c3 ( Procccding~ of the {nternattonal Colloqmum, (Kyoto, Japan?, Aug. ~1990). World Scientific, Singapore, (Mar.).
• 22: Nachum Dershowitz , Jean-Pierre Jouannaud, Rewrite systems, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 23: Nachum Dershowitz , Zohar Manna, Proving termination with multiset orderings, Communications of the ACM, v.22 n.8, p.465-476, Aug. 1979 [doi>10.1145/359138.359142]
• 24: Nachum Dershowitz , Leo Marcus , Andrzej Tarlecki, Existence, uniqueness, and construction of rewrite systems, SIAM Journal on Computing, v.17 n.4, p.629-639, August 1988 [doi>10.1137/0217039]
• 25: ~EVANS, T., 1951. On multiphcative systems defined by generators and relations, I. Proc. ~Cambridge Phzh)3ophical Soctetv 47, 637 649.
• 26: ~FRIBOURG, L., 1985. A superposmon oriented theorem prover. Theoret. Compttt. Scz. 35, ~129 164.
• 27: L. Fribourg, A strong restriction of the inductive completion procedure, Journal of Symbolic Computation, v.8 n.3, p.253-276, Sep. 1989 [doi>10.1016/S0747-7171(89)80069-0]
• 28: ~GALLIER, J., SNYDER, W., NARENDRAN, P., AND PLAISTED, D., 1988. Rigid E-unification is ~ NP-complete. In Proceedings oJ the 3rd Anmtal Symposium on Logic' m Compztter So'tern'e, ~(Edinburgh, Scotland). IEEE, New York, pp. 218-227.
• 29: ~GALLIER, J., SNYDER, W., AND RAATZ, S., 1989. Rigid E-unification and its application to ~equational matings. In Resolutzon of Equations in Algebraic Stl'ztctttres 1: ,4{gebraic technlqttes, H. ~A'it-Kaci and M. Nivet, eds. Academic Press, Orlando, Fla., pp. 151 216.
• 30: Harald Ganzinger, A completion procedure for conditional equations, Journal of Symbolic Computation, v.11 n.1-2, p.51-81, Jan./Feb. 1991 [doi>10.1016/S0747-7171(08)80132-0]
• 31: Joseph A. Goguen, How to Prove Algebraic Inductive Hypotheses Without Induction, Proceedings of the 5th Conference on Automated Deduction, p.356-373, July 08-11, 1980
• 32: ~GRAMLICH, B., 1990. Completion based inductive theorem proving: An abstract framework and ~ its applications. In Proceedings o)t the European Conference on Artificial hltelhgence, (Stockholm, ~Sweden). pp. 314-319.
• 33: Jieh Hsiang , Nachum Dershowitz, Rewrite Methods for Clausal and Non-Clausal Theorem Proving, Proceedings of the 10th Colloquium on Automata, Languages and Programming, p.331-346, July 18-22, 1983
• 34: J. Hsiang , M. Rusinowitch, On word problems in equational theories, 14th International Colloquium on Automata, languages and programming, p.54-71, July 1987, Karlsruhe, Germany
• 35: Gérard Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems, Journal of the ACM (JACM), v.27 n.4, p.797-821, Oct. 1980 [doi>10.1145/322217.322230]
• 36: ~HUET, G., 1981. A complete proof of correctness of the Knuth and Bendix completion ~algorithm. J. Compttt. Syst. Sci. 23, 11 21.
• 37: ~HUET, G., AND HULLOT, J.-M., 1982. Proofs by reduction in equational theories with construc- ~tors..1. Compttt. Syst. Sci. 25, 239-266.
• 38: ~JOUANNAUD, J.-P., 1987. -A set of eleven important open problems in term rewriting based ~ theorem proving. Bttll. Europ. Assoc. Tbeoret. Comput. Sci. 31, (Feb.), 272-273.
• 39: Jean-Pierre Jouannaud , Emmanuel Kounalis, Automatic proofs by induction in theories without constructors, Information and Computation, v.82 n.1, p.1-33, July 1989 [doi>10.1016/0890-5401(89)90062-X]
• 40: Jean-Pierre Jouannaud , Mitsuhiro Okada, Satisfiability of systems of ordinal notations with the subterm property is decidable, Proceedings of the 18th international colloquium on Automata, languages and programming, p.455-468, June 1991, Madrid, Spain
• 41: Deepak Kapur , David R. Musser, Proof by consistency, Artificial Intelligence, v.31 n.2, p.125-157, Feb. 1987 [doi>10.1016/0004-3702(87)90017-8]
• 42: D. Kapur , D. R. Musser , P. Narendran, Only prime superpositions need be considered in the Knuth-Bendix completion procedure, Journal of Symbolic Computation, v.6 n.1, p.19-36, August 1988 [doi>10.1016/S0747-7171(88)80019-1]
• 43: ~KAPUR, D., NARENDRAN, P., ROSENKRANTZ, D. J., AND ZHANG, H., 1987. Sufficient-complete- ~ness, quasi-reducibility and their complexity. Tech. Rep., Dept. Comput. Sci.. SUNY at Albany, ~Albany, N.Y.
• 44: ~KAPUR, D., NARENDRAN, P., AND ZHANG, H., 1987b. On sufficient-completeness and related ~properties of term rewriting systems. Acta Inf. 24, 395 415.
• 45: Deepak Kapur , Paliath Narendran , Hantao Zhang, Automating inductionless induction using test sets, Journal of Symbolic Computation, v.11 n.1-2, p.83-111, Jan./Feb. 1991 [doi>10.1016/S0747-7171(08)80133-2]
• 46: ~KNUTH, D. E., AND BENmX, P. B., 1970. Simple word problems in universal algebras. In ~ Computational Problems in Abstract Algebra, J. Leech, ed., Pergamon Press, Oxford, U.K., pp. ~ 263-297. Reprinted in Automation of Reasomng 2. Springer-Verlag, Berlin, Germany, 1983, pp. ~ 342-376.
• 47: Wolfgang Küchlin, A Confluence Criterion Based on the Generalised Neman Lemma, Research Contributions from the European Conference on Computer Algebra-Volume 2, p.390-399, April 01-03, 1985
• 48: ~KOCHLIN, W., 1986. Equational completion by proof transformation. Ph.D. dissertation. Dept. ~Math. Swiss Federal Institute of Technology, Zurich, Switzerland, June.
• 49: ~KUCHLIN, W., 1989. Inductive completion by ground proof transformation. In Resoltttion of ~Equations in Algebraic Stt~lctltres 2: Rewriting Techniques, H. A'it-Kaci and M. Nivet, eds., ~Academic Press, Orlando, Fla., pp. 211-244.
• 50: ~LANKFORD, D., 1975. Canonical reference. Tech. Rep. ATP-32. Dept. of Math Comput. Scl, ~ Univ. Texas, Austin, Tex.
• 51: ~LANKFORD, D., 1979. On proving term rewriting systems are Noethenan. Tech. Rep. MTP-3. ~Math. Dept. Louisiana Tech. Univ., Ruston, La.
• 52: ~MF2TIV1ER, Y., 1983. About the rewriting systems produced by the Knuth Bendix completion ~algorithm, htf. Proc. Lett. lO, 1 (Jan.). 31 34,
• 53: David R. Musser, On proving inductive properties of abstract data types, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.154-162, January 28-30, 1980, Las Vegas, Nevada [doi>10.1145/567446.567461]
• 54: ~MZALI, J., 1986. Methodes de filtrage equationnel st de preuve automatique de theoremes. ~Ph.D. dissertation. Unlversitd de Nancy, Nancy, France, 1986.
• 55: ~OHSUGA, m., AND SAKAI, K., 1986. Metls: A term rewriting system generator. Tech. Rcpt ~ICOT Research Center, Tokyo, Japan.
• 56: ~PETERSON, G.E., 1983. A technique for establishing completeness results m theorem proving ~with equality. S1AM J. Cornput 12, 82-100.
• 57: Gerald E. Peterson , Mark E. Stickel, Complete Sets of Reductions for Some Equational Theories, Journal of the ACM (JACM), v.28 n.2, p.233-264, April 1981 [doi>10.1145/322248.322251]
• 58: ~PLAISTED, D.A., 1985. Semantic confluence tests and completion methods. Inf. Comput. 65, ~182-215
• 59: U. S. Reddy, Rewriting techniques for program synthesis, Proceedings of the 3rd international conference on Rewriting Techniques and Applications, p.388-403, January 1989
• 60: Uday S. Reddy, Term rewriting induction, Proceedings of the tenth international conference on Automated deduction, p.162-177, July 1990, Kaiserslautern, Germany
• 61: ~ROBINSON, G, AND WOS, L., 1969. Paramodutation and theorem-proving m first order theories ~with equality. In Machine lntelhgence vol. 4, B. Meltzer and D. Michle, cds. Edinburgh ~ University Press, Edinburgh, Scotland, pp, 135-150.
• 62: ~WINKLER, F., AND BUCHBERGER, B., 1983. A criterion for eliminating unnecessary reductions ~ in the Knuth-Bendix algorithm. In Proceedings of the Colloquium on Algebra, Combmatoraz~s and ~Logw in Computer Science (Gy6r, Hungary). J. Bolyaz Math Socwty, pp. 849-869.
• 63: H. Zhang , D. Kapur, Consider only general superpositions in completion procedures, Proceedings of the 3rd international conference on Rewriting Techniques and Applications, p.513-529, January 1989

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Proof theory

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Computational logic; Mechanical theorem proving

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.3 Deduction and Theorem Proving
          Subjects: Metatheory**; Deduction (e.g., natural, rule-based); Mathematical induction

General Terms:
Theory

Keywords:
equational logic, inference systems, proof theory, rewrite systems, term orderings, term rewriting