Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

Non-disjoint Combined Unification and Closure by Equational Paramodulation (Extended Version)

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 :
Preprints, Working Papers, ...
Complete list of metadata
Contributor : Christophe Ringeissen Connect in order to contact the contributor
Submitted on : Monday, August 30, 2021 - 3:52:17 PM
Last modification on : Thursday, March 17, 2022 - 2:51:25 PM


Files produced by the author(s)


  • HAL Id : hal-03329075, version 1



Serdar Erbatur, Andrew M Marshall, Christophe Ringeissen. Non-disjoint Combined Unification and Closure by Equational Paramodulation (Extended Version). 2021. ⟨hal-03329075⟩



Record views


Files downloads