Skip to Main content Skip to Navigation
Conference papers

Terminating Non-Disjoint Combined Unification

Abstract : The equational unification problem, where the underlying equational theory may be given as the union of component equational theories, appears often in practice in many fields such as automated reasoning, logic programming, declarative programming, and the formal analysis of security protocols. In this paper, we investigate the unification problem in the non-disjoint union of equational theories via the combination of hierarchical unification procedures. In this context, a unification algorithm known for a base theory is extended with some additional inference rules to take into account the rest of the theory. We present a simple form of hierarchical unification procedure. The approach is particularly well-suited for any theory where a unification procedure can be obtained in a syntactic way using transformation rules to process the axioms of the theory. Hierarchical unification procedures are exemplified with various theories used in protocol analysis. Next, we look at modularity methods for combining theories already using a hierarchical approach. In addition, we consider a new complexity measure that allows us to obtain terminating (combined) hierarchical unification procedures.
Document type :
Conference papers
Complete list of metadata
Contributor : Christophe Ringeissen Connect in order to contact the contributor
Submitted on : Friday, December 11, 2020 - 4:06:26 PM
Last modification on : Wednesday, November 3, 2021 - 7:56:47 AM


Files produced by the author(s)




Serdar Erbatur, Andrew Marshall, Christophe Ringeissen. Terminating Non-Disjoint Combined Unification. LOPSTR 2020 - 30th International Symposium on Logic-based Program Synthesis and Transformation, Maurizio Gabbrielli, Sep 2020, Bologna, Italy. pp.113-130, ⟨10.1007/978-3-030-68446-4_6⟩. ⟨hal-02967029v2⟩



Les métriques sont temporairement indisponibles