Theorem proving with bounded rigid E-unification
2015 (English)In: Automated Deduction – CADE-25: 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, Springer, 2015, 572-587 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 80 s and 90s. However, the fact that simultaneous rigid E-unification is undecidable has limited practical adoption, and to the best of our knowledge there is no tableau-based theorem prover that uses rigid E-unification. We introduce simultaneous bounded rigid E-unification (BREU), a new version of rigid E-unification that is bounded in the sense that variables only represent terms from finite domains. We show that (simultaneous) BREU is NP-complete, outline how BREU problems can be encoded as propositional SAT-problems, and use BREU to introduce a sound and complete sequent calculus for first-order logic with equality.
Place, publisher, year, edition, pages
Springer, 2015. 572-587 p.
, Lecture Notes in Computer Science, ISSN 0302-9743 ; 9195
Computer Science Robotics
IdentifiersURN: urn:nbn:se:uu:diva-268734DOI: 10.1007/978-3-319-21401-6_39ISBN: 978-3-319-21400-9OAI: oai:DiVA.org:uu-268734DiVA: diva2:878798
25th International Conference on Automated Deduction, August 1-7, 2015, Berlin, Germany
FunderSwedish Research Council, 2014-5484