Terminating Non-Disjoint Combined Unification

Serdar Erbatur (1) , Andrew M Marshall (2) , Christophe Ringeissen (3)

1 University of Texas at Dallas - Department of Computer Science [Dallas]
2 University of Mary Washington
3 PESTO - Proof techniques for security protocols

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.

Domaines: Logique en informatique [cs.LO]

Serdar Erbatur, Andrew M 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⟩