Abstract
We present a completion-based method for handling a new version of E- unification, called “mixed” E-unification, that is a combination of the classical “universal” E-unification and “rigid” E-unification. Rigid E-unification is an important method for handling equality in Gentzen-type first-order calculi, such as free-variable semantic tableaux or matings. The performance of provers using E-unification can be increased considerably, if mixed E-unification is used instead of the purely rigid version. We state soundness and completeness results, and describe experiments with an implementation of our method.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
L. Bachmair, N. Dershowitz, and D. Plaisted. Completion without failure. In H. AÏt-Kaci and M. Nivat, editors, Resolution of Equations in Algebraic Structures, Volume 2, chapter 1. Academic Press, 1989.
B. Beckert. Ein vervollständigungsbasiertes Verfahren zur Behandlung von Gleichheit im Tableaukalkül mit freien Variablen. Diploma thesis, Univ. Karlsruhe, 1993.
B. Beckert, S. Gerberding, R. Hähnle, and W. Kernig. The tableau-based theorem prover 3 T A P for multiple-valued logics. In Proceedings, 11th International Conference on Automated Deduction (CADE), Albany/NY, LNCS. Springer, 1992.
B. Beckert and R. Hähnle. An improved method for adding equality to free variable semantic tableaux. In Proceedings, 11th International Conference on Automated Deduction (CADE), Albany/NY, LNCS. Springer, 1992.
J. Chabin, S. Anantharaman, and P. Réty. E-unification via constrained rewriting. Unpublished, 1993.
H. Comon. Solving inequations in term algebras. In Proceedings, 5th Symposium on Logic in Computer Science (LICS), Philadelphia/PA. IEEE Press, 1990.
N. Dershowitz. Termination of rewriting. J. of Symbolic Computation, 3(1), 1987.
J. Gallier, P. Narendran, D. Plaisted, and W. Snyder. Rigid E-unification: NP-completeness and application to equational matings. Information and Computation, pages 129–195, 1990.
J. Gallier, P. Narendran, S. Raatz, and W. Snyder. Theorem proving using equational matings and rigid E-unification. Journal of the ACM, 39(2), 1992.
J. Goubault. Simultaneous rigid E-unifiability is NEXPTIME-complete. Technical report, Bull Corporate Research Center, 1993.
J. Hsiang and J. Mzali. SbREVE user's guide. Technical report, LRI, Université de Paris-Sud, 1988.
C. Kirchner, editor. Unification. Academic Press, 1990.
D. E. Knuth and P. B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebras. Pergamon Press, Oxford, 1970.
W. Nutt, P. Réty, and G. Smolka. Basic narrowing revisited. Journal of Symbolic Computation, 7(3/4):295–318, 1989.
U. Petermann. A framework for integrating equality reasoning into the extension procedure. In Proc, 2nd Workshop on Theorem Proving with Analytic Tableaux and Related Methods, Marseille. MPI für Informatik, 92–213, Saarbrücken, 1993.
G. Peterson. Complete sets of reductions with constraints. In Proceedings, 10th International Conference on Automated Deduction (CADE), Kaiserslautern, LNCS. Springer, 1990.
J. Siekmann. Universal unification. Jour. of Symbolic Computation, 7(3/4), 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Beckert, B. (1994). A completion-based method for mixed universal and rigid E-unification. In: Bundy, A. (eds) Automated Deduction — CADE-12. CADE 1994. Lecture Notes in Computer Science, vol 814. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58156-1_49
Download citation
DOI: https://doi.org/10.1007/3-540-58156-1_49
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58156-7
Online ISBN: 978-3-540-48467-7
eBook Packages: Springer Book Archive