Anzeige
Erschienen in:
2015 | OriginalPaper | Buchkapitel
Efficient Algorithms for Bounded Rigid E-unification
verfasst von : Peter Backeman, Philipp Rümmer
Erschienen in: Automated Reasoning with Analytic Tableaux and Related Methods
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.