Abstract canonical inference

ABSTRACT

An abstract framework of canonical inference is used to explore how different proof orderings induce different variants of saturation and completeness. Notions like completion, paramodulation, saturation, redundancy elimination, and rewrite-system reduction are connected to proof orderings. Fairness of deductive mechanisms is defined in terms of proof orderings, distinguishing between (ordinary) “fairness,” which yields completeness, and “uniform fairness,” which yields saturation.

REFERENCES

• 1: 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]
• 2: 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]
• 3: Leo Bachmair , Nachum Dershowitz, Equational inference, canonical proofs, and proof orderings, Journal of the ACM (JACM), v.41 n.2, p.236-276, March 1994 [doi>10.1145/174652.174655]
• 4: Bachmair, L., Dershowitz, N., and Plaisted, D. A. 1989. Completion without failure. In Resolution of Equations in Algebraic Structures, vol. 2:1 Rewriting Techniques. H. Aït-Kaci and M. Nivat, eds. Academic Press, London, 1--30.
• 5: Bachmair, L. and Ganzinger, H. 1994. Rewrite-Based equational theorem proving with selection and simplification. J. Logic Comput. 4, 3, 217--247.
• 6: Bachmair, L. and Ganzinger, H. 2001. Resolution theorem proving. In Handbook of Automated Reasoning, vol. 1. A. Robinson and A. Voronkov, eds. Elsevier Science, Amsterdam, 19--99.
• 7: Leo Bachmair , Ashish Tiwari , Laurent Vigneron, Abstract Congruence Closure, Journal of Automated Reasoning, v.31 n.2, p.129-168, 2003 [doi>10.1023/B:JARS.0000009518.26415.49]
• 8: Maria Paola Bonacina, Distributed automated deduction, State University of New York at Stony Brook, Stony Brook, NY, 1992
• 9: Bonacina, M. P. 1999. A taxonomy of theorem-proving strategies. In Artificial Intelligence Today -- Recent Trends and Developments, M. J. Wooldridge and M. Veloso, eds. Lecture Notes in Artificial Intelligence, vol. 1600. Springer-Verlag, Berlin, 43--84.
• 10: Maria Paola Bonacina , Jieh Hsiang, On rewrite programs: semantics and relationship with Prolog, Journal of Logic Programming, v.14 n.1-2, p.155-180, Oct., 1992 [doi>10.1016/0743-1066(92)90050-D]
• 11: Maria Paola Bonacina , Jieh Hsiang, Towards a foundation of completion procedures as semidecision procedures, Theoretical Computer Science, v.146 n.1-2, p.199-242, July 24, 1995 [doi>10.1016/0304-3975(94)00187-N]
• 12: Brown, Jr., T. C. 1975. A structured design-method for specialized proof procedures. Ph.D. thesis, California Institute of Technology, Pasadena, CA.
• 13: Buchberger, B. 1985. Multidimensional Systems Theory. Reidel, Bose, N.K. ed., 184--232.
• 14: Burel, G. and Kirchner, C. 2006. Completion is an instance of abstract canonical system inference. In Algebra, Meaning and Computation -- Essays in Honor of Joseph Goguen, K. Futatsugi, J.-P. Jouannaud, and J. Meseguer, Eds. Vol. 4060. Springer-Verlag, 497--520.
• 15: Dershowitz, N. 1982. Orderings for term-rewriting systems. Theor. Comput. Sci. 17, 3 (Mar.), 279--301.
• 16: Dershowitz, N. 1985. Computing with rewrite systems. Inf. Control 64, 2--3 (May--Jun.), 122--157.
• 17: Dershowitz, N. 1989. Completion and its applications. In Resolution of Equations in Algebraic Structures, vol. 2: Rewriting Techniques, H. Aït-Kaci and M. Nivat, eds. Academic Press, London, 31--86.
• 18: Nachum Dershowitz, Cononical Sets of Horn Clauses, Proceedings of the 18th International Colloquium on Automata, Languages and Programming, p.267-278, July 08-12, 1991
• 19: Dershowitz, N. 1991b. Ordering-Based strategies for Horn clauses. In Proceedings of the 12th International Joint Conference on Artificial Intelligence. (Sydney, Australia). Morgan Kaufmann, San Fransisco, CA, 118--124.
• 20: Nachum Dershowitz , Claude Kirchner, Abstract canonical presentations, Theoretical Computer Science, v.357 n.1, p.53-69, 25 July 2006 [doi>10.1016/j.tcs.2006.03.012]
• 21: 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]
• 22: Dershowitz, N. and Plaisted, D. A. 2001. Rewriting. In Handbook of Automated Reasoning, vol. 1. A. Robinson and A. Voronkov, eds. Elsevier Science, Amsterdam, 535--610.
• 23: Nachum Dershowitz , Uday S. Reddy, Deductive and inductive synthesis of equational programs, Journal of Symbolic Computation, v.15 n.5-6, p.467-494, May/June 1993 [doi>10.1016/S0747-7171(06)80002-7]
• 24: Narjes Doggaz , Claude Kirchner, Completion for unification, Theoretical Computer Science, v.85 n.2, p.231-251, Aug. 12, 1991 [doi>10.1016/0304-3975(91)90182-2]
• 25: 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]
• 26: Jean Gallier , Paliath Narendran , David Plaisted , Stan Raatz , Wayne Snyder, An algorithm for finding canonical sets of ground rewrite rules in polynomial time, Journal of the ACM (JACM), v.40 n.1, p.1-16, Jan. 1993 [doi>10.1145/138027.138032]
• 27: Hillenbrand, T. 2003. Citius, altius, fortius: Lessons learned from the theorem prover waldmeister. In Proceedings of the 4th International Workshop On First-Order Theorem Proving (FTP), I. Dahn and L. Vigneron, eds. Electronic Notes in Theoretical Computer Science, vol. 86. Elsevier. http://www.sciencedirect.com.
• 28: Jieh Hsiang , Michaël Rusinowitch, On Word Problems in Equational Theories, Proceedings of the 14th International Colloquium, on Automata, Languages and Programming, p.54-71, July 13-17, 1987
• 29: Jieh Hsiang , Michaël Rusinowitch, Proving refutational completeness of theorem-proving strategies: the transfinite semantic tree method, Journal of the ACM (JACM), v.38 n.3, p.558-586, July 1991 [doi>10.1145/116825.116833]
• 30: Huet, G. 1981. A complete proof of correctness of the Knuth--Bendix completion algorithm. J. Comput. Syst. Sci. 23, 1 (Aug.), 11--21.
• 31: Jean-Pierre Jouannaud , Hélène Kirchner, Completion of a set of rules modulo a set of equations, SIAM Journal on Computing, v.15 n.4, p.1155-1194, Nov. 1986 [doi>10.1137/0215084]
• 32: 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]
• 33: Knuth, D. E. and Bendix, P. B. 1970. Simple word problems in universal algebras. In Computational Problems in Abstract Algebra, J. Leech, ed. Pergamon Press, Oxford, UK. 263--297.
• 34: Emmanuel Kounalis , Michael Rusinowitch, On word problems in horn theories, Journal of Symbolic Computation, v.11 n.1-2, p.113-127, Jan./Feb. 1991 [doi>10.1016/S0747-7171(08)80134-4]
• 35: Lankford, D. S. 1975. Canonical inference. Memo ATP-32, Automatic Theorem Proving Project, University of Texas, Austin, TX. Dec.
• 36: McCune, W. W. 1994. Otter 3.0 reference manual and guide. Tech. Rep. 94/6, MCS Division, Argonne National Laboratory. http://www-unix.mcs.anl.gov/AR/otter/.
• 37: Metivier, Y. 1983. About the rewriting systems produced by the Knuth-Bendix completion algorithm. Inf. Process. Lett. 16, 1 (Jan.), 31--34.
• 38: Nieuwenhuis, R. and Rubio, A. 2001. Paramodulation-based theorem proving. In Handbook of Automated Reasoning, vol. 1. A. Robinson and A. Voronkov, eds. Elsevier Science, Amsterdam, 371--443.
• 39: 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]
• 40: David A. Plaisted , Andrea Sattler-Klein, Proof lengths for equational completion, Information and Computation, v.125 n.2, p.154-170, March 15, 1996 [doi>10.1006/inco.1996.0028]
• 41: Alexandre Riazanov , Andrei Voronkov, The design and implementation of VAMPIRE, AI Communications, v.15 n.2, p.91-110, September 2002
• 42: Robinson, G. and Wos, L. 1969. Paramodulation and theorem-proving in first-order theories with equality. In Machine Intelligence, vol. 4. D. Michie and R. Meltzer, eds. Edinburgh University Press, Edinburgh, UK. 135--150.
• 43: Michael Rusinowitch, Theorem-proving with resolution and superposition, Journal of Symbolic Computation, v.11 n.1-2, p.21-49, Jan./Feb. 1991 [doi>10.1016/S0747-7171(08)80131-9]
• 44: Stephan Schulz, E - a brainiac theorem prover, AI Communications, v.15 n.2, p.111-126, September 2002
• 45: Tanel Tammet, Gandalf, Journal of Automated Reasoning, v.18 n.2, p.199-204, April 1997 [doi>10.1023/A:1005887414560]
• 46: Terese. 2003. Term Rewriting Systems, M. Bezem et al., eds. Cambridge University Press, Cambridge, UK.
• 47: Christoph Weidenbach, System Description: Spass Version 1.0.0, Proceedings of the 16th International Conference on Automated Deduction: Automated Deduction, p.378-382, July 07-10, 1999

INDEX TERMS

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

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.2 Grammars and Other Rewriting Systems
          Subjects: Decision problems

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.3 Deduction and Theorem Proving
          Subjects: Inference engines

General Terms:
Theory

Keywords:
Inference, canonicity, completeness, completion, fairness, proof orderings, redundancy, saturation