Abstract
The efficient integration of theory reasoning in first-order calculi with free variables (such as sequent calculi or tableaux) is a long-standing challenge. For the case of the theory of equality, an approach that has been extensively studied in the 90s is rigid E-unification, a variant of equational unification in which the assumption is made that every variable denotes exactly one term (rigid semantics). The fact that simultaneous rigid E-unification is undecidable, however, has hampered practical adoption of the method, and today there are few theorem provers that use rigid E-unification.
One solution is to consider incomplete algorithms for computing (simultaneous) rigid E-unifiers, which can still be sufficient to create sound and complete theorem provers for first-order logic with equality; such algorithms include rigid basic superposition proposed by Degtyarev and Voronkov, but also the much older subterm instantiation approach introduced by Kanger in 1963 (later also termed minus-normalisation). We introduce bounded rigid E-unification (BREU) as a new variant of E-unification corresponding to subterm instantiation. In contrast to general rigid E-unification, BREU is NP-complete for individual and simultaneous unification problems, and can be solved efficiently with the help of SAT; BREU can be combined with techniques like congruence closure for ground reasoning, and be used to construct theorem provers that are competitive with state-of-the-art tableau systems. We outline ongoing research how BREU can be generalised to other theories than equality.
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.
Similar content being viewed by others
References
Backeman, P., Rümmer, P.: Efficient algorithms for bounded rigid E-Unification. In: Tableaux. LNCS. Springer (to appear, 2015)
Backeman, P., Rümmer, P.: Theorem proving with bounded rigid E-Unification. In: CADE. LNCS. Springer (to appear, 2015)
Degtyarev, A., Voronkov, A.: Simultaneous rigid E-Unification is undecidable. In: Kleine Büning, H. (ed.) CSL 1995. LNCS, vol. 1092, pp. 178–190. Springer, Heidelberg (1996)
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, vol. 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)
Giese, M.A.: A model generation style completeness proof for constraint tableaux with superposition. In: Egly, U., Fermüller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol. 2381, pp. 130–144. Springer, Heidelberg (2002)
Halpern, J.Y.: Presburger arithmetic with unary predicates is \(\Pi_1^1\) complete. Journal of Symbolic Logic 56 (1991)
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
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). Free Variables and Theories: Revisiting Rigid E-unification. In: Lutz, C., Ranise, S. (eds) Frontiers of Combining Systems. FroCoS 2015. Lecture Notes in Computer Science(), vol 9322. Springer, Cham. https://doi.org/10.1007/978-3-319-24246-0_1
Download citation
DOI: https://doi.org/10.1007/978-3-319-24246-0_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-24245-3
Online ISBN: 978-3-319-24246-0
eBook Packages: Computer ScienceComputer Science (R0)