Advertisement

Elimination of equality via transformation with ordering constraints

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

Abstract

We refine Brand's method for eliminating equality axioms by (i) imposing ordering constraints on auxiliary variables introduced during the transformation process and (ii) avoiding certain transformations of positive equations with a variable on one side. The refinements are both of theoretical and practical interest. For instance, the second refinement is implemented in Setheo and appears to be critical for that prover's performance on equational problems. The correctness of this variant of Brand's method was an open problem that is solved by the more general results in the present paper. The experimental results we obtained from a prototype implementation of our proposed method also show some dramatic improvements of the proof search in model elimination theorem proving. We prove the correctness of our refinements of Brand's method by establishing a suitable connection to basic paramodulation calculi and thereby shed new light on the connection between different approaches to equational theorem proving.

Keywords

Transformation Rule Model Elimination Ground Instance Unit Clause Proof Search 
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.

erences

  1. 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
  2. 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
  3. Baumgartner, P. & Furbach, U. (1994), PROTEIN: A PROver with a Theory Extension INterface, in A. Bundy, ed., ‘Automated Deduction — CADE-12. 12th International Conference on Automated Deduction.', Vol. 814 of Lecture Notes in Artificial Intelligence, Nancy, France, pp. 769–773.Google Scholar
  4. Brand, D. (1975), ‘Proving theorems with the modification method', SIAM Journal of Computing 4, 412–430.zbMATHMathSciNetCrossRefGoogle Scholar
  5. Degtyarev, A. & Voronkov, A. (1996a), Equality elimination for the tableau method, in J. Calmet & C. Limongelli, eds, ‘Design and Implementation of Symbolic Computation Systems. International Symposium, DISCO'96', Vol. 1128 of Lecture Notes in Computer Science, Karlsruhe, Germany, pp. 46–60.Google Scholar
  6. Degtyarev, A. & Voronkov, A. (1996b), What you always wanted to know about rigid E-unification, in J. Alferes, L. Pereira & E. Orlowska, eds, ‘Logics in Artificial Intelligence. European Workshop, JELIA'96', Vol. 1126 of Lecture Notes in Artificial Intelligence, évora, Portugal, pp. 50–69.Google Scholar
  7. Ibens, O. & Letz, R. (1997), Subgoal alternation in model elimination, in D. Galmiche, ed., ‘Automated Reasoning with Analytic Tableaux and Related Methods', Vol. 1227 of Lecture Notes in Artificial Intelligence, Springer Verlag, pp. 201–215.Google Scholar
  8. Moser, M., Lynch, C. & Steinbach, J. (1995), Model elimination with basic ordered paramodulation, Technical Report AR-95-11, FakultÄt für Informatik, Technische UniversitÄt München, München.Google Scholar
  9. Moser, M. & Steinbach, J. (1997), STE-modification revisited, Technical Report AR-97-03, FakultÄt für Informatik, Technische UniversitÄt München, München.Google Scholar
  10. Schumann, J. (1994), ‘Tableau-based theorem provers: Systems and implementations', Journal of Automated Reasoning 13(3), 409–421.MathSciNetCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Leo Bachmair
    • 1
  • Harald Ganzinger
    • 2
  • Andrei Voronkov
    • 3
  1. 1.Comp. Sci. Dept.SUNY at Stony BrookUSA
  2. 2.MPI InformatikSaarbrückenGermany
  3. 3.Comp. Sci. Dept.Uppsala U.UppsalaSweden

Personalised recommendations