Advertisement

Strict basic superposition

  • Leo Bachmair
  • Harald Ganzinger
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1421)

Abstract

In this paper we solve a long-standing open problem by showing that strict superposition—that is, superposition without equality factoring—is refutationally complete. The difficulty of the problem arises from the fact that the strict calculus, in contrast to the standard calculus with equality factoring, is not compatible with arbitrary removal of tautologies, so that the usual techniques for proving the (refutational) completeness of paramodulation calculi are not directly applicable. We deal with the problem by introducing a suitable notion of direct rewrite proof and modifying proof techniques based on candidate models and counterexamples in that we define these concepts in terms of, not semantic truth, but direct provability. We introduce a corresponding concept of redundancy with which strict superposition is compatible and that covers most simplification techniques. We also show that certain superposition inferences from variables are redundant—a result that is relevant, surprisingly, in the context of equality elimination methods.

Keywords

Candidate Model Theorem Prove Automate Deduction Maximal Term Empty Clause 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bachmair, L. & Ganzinger, H. (1990), On restrictions of ordered paramodulation with simplification, in M. Stickel, ed., ‘Proc. 10th Int. Conf. on Automated Deduction, Kaiserslautern', Vol. 449 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 427–441.Google Scholar
  2. Bachmair, L. & Ganzinger, H. (1994), ‘Rewrite-based equational theorem proving with selection and simplification', J. Logic and Computation 4(3), 217–247. Revised version of Technical Report MPI-I-91-208, 1991.MathSciNetzbMATHGoogle Scholar
  3. Bachmair, L. & Ganzinger, H. (1995), Ordered chaining calculi for first-order theories of binary relations, Research Report MPI-I-95-2-009, Max-Planck-Institut für Informatik, Saarbrücken, Saarbrücken. Revised version to appear in JACM. URL: www.mpi-sb.mpg.de/~hg/pra.html#MPI-I-95-2-009Google Scholar
  4. Bachmair, L. & Ganzinger, H. (1997), Strict basic superposition and chaining, Research Report MPI-I-97-2-011, Max-Planck-Institut für Informatik, Saarbrücken, Saarbrücken. URL: www.mpi-sb.mpg.de/~hg/pra.html#MPI-I-97-2-011Google Scholar
  5. Bachmair, L., Ganzinger, H., Lynch, C. & Snyder, W. (1992), Basic paramodulation and superposition, in D. Kapur, ed., ‘Automated Deduction — CADE'11', Vol. 607 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 462–476.Google Scholar
  6. Bachmair, L., Ganzinger, H. & Voronkov, A. (1997), Elimination of equality via transformation with ordering constraints, Research Report MPI-I-97-2-012, Max-Planck-Institut für Informatik, Saarbrücken, Saarbrücken. URL: www.mpi-sb.mpg.de/~hg/pra.html#MPI-I-97-2-012Google Scholar
  7. Brand, D. (1975), ‘Proving theorems with the modification method', SIAM J. Comput. 4, 412–430.zbMATHCrossRefMathSciNetGoogle Scholar
  8. Nieuwenhuis, R. & Rubio, A. (1992a), Basic superposition is complete, in ‘ESOP'92', Vol. 582 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 371–389.Google Scholar
  9. Nieuwenhuis, R. & Rubio, A. (1992b), Theorem proving with ordering constrained clauses, in ‘Automated Deduction — CADE'11', Vol. 607 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 477–491.Google Scholar
  10. Pais, J. & Peterson, G. (1991), ‘Using forcing to prove completeness of resolution and paramodulation', J. Symbolic Computation 11, 3–19.MathSciNetCrossRefzbMATHGoogle Scholar
  11. Zhang, H. (1988), Reduction, superposition and induction: Automated reasoning in an equational logic, PhD thesis, Rensselaer Polytechnic Institute, Schenectady, New York.Google Scholar
  12. Zhang, H. & Kapur, D. (1988), First-order theorem proving using conditional rewrite rules, in E. Lusk & R. Overbeek, eds, ‘Proc. 9th Int. Conf. on Automated Deduction', Vol. 310 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 1–20.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Leo Bachmair
    • 1
  • Harald Ganzinger
    • 2
  1. 1.Comp. Sci. Dept.SUNY at Stony BrookUSA
  2. 2.MPI InformatikSaarbrückenGermany

Personalised recommendations