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 show theories for which a hierarchical approach is applicable and 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 metadatas

Cited literature [32 references]  Display  Hide  Download

https://hal.inria.fr/hal-02967029
Contributor : Christophe Ringeissen <>
Submitted on : Wednesday, October 14, 2020 - 4:08:38 PM
Last modification on : Thursday, October 15, 2020 - 4:10:18 AM

File

combi-hu.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02967029, version 1

Collections

Citation

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. ⟨hal-02967029⟩

Share

Metrics

Record views

15

Files downloads

20