Efficient algorithms for bounded rigid E-unification
2015 (English)In: Automated Reasoning with Analytic Tableaux and Related Methods: 24th International Conference, TABLEAUX 2015, Wroclaw, Poland, September 21-24, 2015, Proceedings, Springer, 2015, 70-85 p.Conference paper (Refereed)
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.
Place, publisher, year, edition, pages
Springer, 2015. 70-85 p.
, Lecture Notes in Computer Science, ISSN 0302-9743 ; 9323
IdentifiersURN: urn:nbn:se:uu:diva-268735DOI: 10.1007/978-3-319-24312-2_6ISI: 000366125200009ISBN: 978-3-319-24311-5OAI: oai:DiVA.org:uu-268735DiVA: diva2:878801
TABLEAUX 2015, September 21–24, Wroclaw, Poland
FunderSwedish Research Council, 2014-5484