Abstract
Rigid E-unification is the problem of unifying two expressions modulo a set of equations, with the assumption that every variable denotes exactly one term (rigid semantics). This form of unification was originally developed as an approach to integrate equational reasoning in tableau-like proof procedures, and studied extensively in the late 80s and 90s. However, the fact that simultaneous rigid E-unification is undecidable has limited the practical relevance of the method, and to the best of our knowledge there is no tableau-based theorem prover that uses rigid E-unification. We recently introduced a new decidable variant of (simultaneous) rigid E-unification, bounded rigid E-unification (BREU), in which variables only represent terms from finite domains, and used it to define a first-order logic calculus. In this paper, we study the problem of computing solutions of (individual or simultaneous) BREU problems. Two new unification procedures for BREU are introduced, and compared theoretically and experimentally.
This work was partly supported by the Microsoft PhD Scholarship Programme and the Swedish Research Council.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bachmair, L., Tiwari, A., Vigneron, L.: Abstract congruence closure. J. Autom. Reasoning 31(2), 129–168 (2003)
Backeman, P., Rümmer, P.: Theorem proving with bounded rigid E-Unification. In: CADE. LNCS. Springer (2015, to appear)
Degtyarev, A., Voronkov, A.: What you always wanted to know about rigid E-Unification. J. Autom. Reasoning 20(1), 47–80 (1998)
Degtyarev, A., Voronkov, A.: Equality reasoning in sequent-based calculi. In: Handbook of Automated Reasoning, vols. 2. Elsevier and MIT Press (2001)
Degtyarev, A., Voronkov, A.: Kanger’s Choices in Automated Reasoning. Springer (2001)
Fitting, M.C.: First-Order Logic and Automated Theorem Proving, 2nd edn. Graduate Texts in Computer Science. Springer, Berlin (1996)
Gallier, J.H., Raatz, S., Snyder, W.: Theorem proving using rigid e-unification equational matings. In: LICS, pp. 338–346. IEEE Computer Society (1987)
Kanger, S.: A simplified proof method for elementary logic. In: Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning 1: Classical Papers on Computational Logic 1957–1966, pp. 364–371. Springer, Heidelberg (1983) (originally appeared in 1963)
Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM 27, 356–364 (1980)
Rümmer, P.: A constraint sequent calculus for first-order logic with linear integer arithmetic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 274–289. Springer, Heidelberg (2008)
Tiwari, A., Bachmair, L., Rueß, H.: Rigid E-Unification revisited. In: CADE, CADE-17, pp. 220–234. Springer, London (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Backeman, P., Rümmer, P. (2015). Efficient Algorithms for Bounded Rigid E-unification. In: De Nivelle, H. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2015. Lecture Notes in Computer Science(), vol 9323. Springer, Cham. https://doi.org/10.1007/978-3-319-24312-2_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-24312-2_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-24311-5
Online ISBN: 978-3-319-24312-2
eBook Packages: Computer ScienceComputer Science (R0)