Skip to Main content Skip to Navigation
New interface
Conference papers

Non-disjoint Combined Unification and Closure by Equational Paramodulation

Abstract : Closure properties such as forward closure and closure via paramodulation have proven to be very useful in equational logic, especially for the formal analysis of security protocols. In this paper, we consider the non-disjoint unification problem in conjunction with these closure properties. Given a base theory E, we consider classes of theory extensions of E admitting a unification algorithm built in a hierarchical way. In this context, a hierarchical unification procedure is obtained by extending an E-unification algorithm with some additional inference rules to take into account the rest of the theory. We look at hierarchical unification procedures by investigating an appropriate notion of E-constructed theory, defined in terms of E-paramodulation. We show that any E-constructed theory with a finite closure by E-paramodulation admits a terminating hierarchical unification procedure. We present modularity results for the unification problem modulo the union of E-constructed theories sharing only symbols in E. Finally, we also give sufficient conditions for obtaining terminating (combined) hierarchical unification procedures in the case of regular and collapse-free E-constructed theories.
Document type :
Conference papers
Complete list of metadata
Contributor : Christophe Ringeissen Connect in order to contact the contributor
Submitted on : Thursday, September 16, 2021 - 2:12:23 PM
Last modification on : Friday, November 18, 2022 - 9:27:25 AM

Links full text




Serdar Erbatur, Andrew Marshall, Christophe Ringeissen. Non-disjoint Combined Unification and Closure by Equational Paramodulation. FroCos 2021 - 13th International Symposium on Frontiers of Combining Systems, Sep 2021, Birmingham, United Kingdom. pp.25-42, ⟨10.1007/978-3-030-86205-3_2⟩. ⟨hal-03346531⟩



Record views