Ordered chaining calculi for first-order theories of transitive relations

ABSTRACT

We propose inference systems for binary relations that satisfy composition laws such as transitivity. Our inference mechanisms are based on standard techniques from term rewriting and represent a refinement of chaining methods as they are used in the context of resolution-type theorem proving. We establish the refutational completeness of these calculi and prove that our methods are compatible with the usual simplification techniques employed in refutational theorem provers, such as subsumption or tautology deletion. Various optimizations of the basic chaining calculus will be discussed for theories with equality and for total orderings. A key to the practicality of chaining methods is the extent to which so-called variable chaining can be avoided. We demonstrate that rewrite techniques considerably restrict variable chaining and that further restrictions are possible if the transitive relation under consideration satisfies additional properties, such as symmetry. But we also show that variable chaining cannot be completely avoided in general.

REFERENCES

• 1: BACHMAIR, L., DERSHOWITZ, N., AND HSIANG, J. 1986. Orderings for equational proofs. In Proceedings of the Symposium on Logic in Computer Science (Boston, Mass.). pp. 346-357.
• 2: BACHMAIR, L., DERSHOWITZ, N., AND PLAISTED, D. 1989. Completion without failure. In Resolution of Equations in Algebraic Structures, vol. 2, H. Ait-Kaci and M. Nivat, eds. Academic Press, Orlando, Fla., pp. 1-30.
• 3: 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
• 4: BACHMAIR, L., AND GANZINGER, H. 1994. Rewrite-based equational theorem proving with selection and simplification. J. Logic Comput. 4, 3, 217-247. (Revised version of Tech. Rep. MPI-I-91- 208, 1991.)
• 5: BACHMAIR, L., AND GANZINGER, H. 1995. Ordered chaining calculi for first-order theories of binary relations. Res. Rep. MPI-I-95-2-009. Max-Planck-Institut ffir Informatik, Saarbrticken, Germany.
• 6: BACHMAIR, L., AND GANZINGER, H. 1999. A theory of resolution. Handb. Autom. Reas., Alan Robinson and Andrei Voronkov, eds. Elsevier Science Publishers.
• 7: Leo Bachmair , Harald Ganzinger , Jürgen Stuber, Combining Algebra and Universal Algebra in First-Order Theorem Proving: The Case of Commutative Rings, Selected papers from the 10th Workshop on Specification of Abstract Data Types Joint with the 5th COMPASS Workshop on Recent Trends in Data Type Specification, p.1-29, May 30-June 03, 1994
• 8: W. W. Bledsoe , K. Kunen , R. Shostak, Completeness results for inequality provers, Artificial Intelligence, v.27 n.3, p.255-288, Dec. 1985 [doi>10.1016/0004-3702(85)90015-3]
• 9: R. S. Boyer , J. S. Moore, Integrating decision procedures into heuristic theorem provers: a case study of linear arithmetic, Machine intelligence 11, Oxford University Press, Inc., New York, NY, 1988
• 10: 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]
• 11: Nachum Dershowitz, A Maximal-Literal Unit Strategy for Horn Clauses, Proceedings of the 2nd International CTRS Workshop on Conditional and Typed Rewriting Systems, p.14-25, June 11-14, 1990
• 12: 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]
• 13: GANZlNGER, H., NIEUWENHUIS, R., AND NIVELA, P. 1994. The Saturate system. User manual maintained on the Web.
• 14: Larry M. Hines, Completeness of a prover for dense linear orders, Journal of Automated Reasoning, v.8 n.1, p.45-75, Feb. 1992
• 15: Larry M. Hines, Str+ve and Integers, Proceedings of the 12th International Conference on Automated Deduction, p.416-430, June 26-July 01, 1994
• 16: Jordi Levy , Jaume Agustí-Cullell, Bi-rewriting, a Term Rewriting Technique for Monotonic Order Relations, Proceedings of the 5th International Conference on Rewriting Techniques and Applications, p.17-31, June 16-18, 1993
• 17: Zohar Manna , Richard Waldinger, Special relations in automated deduction, Journal of the ACM (JACM), v.33 n.1, p.1-59, Jan. 1986 [doi>10.1145/4904.4905]
• 18: Zohar Manna , Richard J. Waldinger, The Special-Relation Rules are Incomplete, Proceedings of the 11th International Conference on Automated Deduction: Automated Deduction, p.492-506, June 15-18, 1992
• 19: Sam Owre , John M. Rushby , Natarajan Shankar, PVS: A Prototype Verification System, Proceedings of the 11th International Conference on Automated Deduction: Automated Deduction, p.748-752, June 15-18, 1992
• 20: Michael M. Richter, Some reordering properties for inequality proof trees, Proceedings of the Symposium "Rekursive Kombinatorik" on Logic and Machines: Decision Problems and Complexity, p.183-197, May 23-28, 1983
• 21: SCOTT, D. S. 1979. Identity and existence in intuitionistic logic. In Applications of Sheaves, Proceedings Durham. Lecture Notes in Mathematics, vol. 753. Springer-Verlag, New York, pp. 660-695.
• 22: James R. Slagle, Automatic Theorem Proving with Built-in Theories Including Equality, Partial Ordering, and Sets, Journal of the ACM (JACM), v.19 n.1, p.120-135, Jan. 1972 [doi>10.1145/321679.321689]
• 23: Uwe Waldmann, Superposition for Divisible Torsion-Free Abelian Groups, Proceedings of the 15th International Conference on Automated Deduction: Automated Deduction, p.144-159, July 05-10, 1998
• 24: Christoph Weidenbach, SPASS - Version 0.49, Journal of Automated Reasoning, v.18 n.2, p.247-252, April 1997 [doi>10.1023/A:1005812220011]

INDEX TERMS

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

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

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.3 Deduction and Theorem Proving
          Subjects: Resolution; Deduction (e.g., natural, rule-based); Inference engines

General Terms:
Theory

Keywords:
chaining calculi, equational logic, reduction orderings, rewrite systems, term rewriting, transitive relations