Non-disjoint Combined Unification and Closure by Equational Paramodulation

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

1 UT Dallas - University of Texas at Dallas [Richardson]
2 University of Mary Washington
3 PESTO - Proof techniques for security protocols

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.

Domaines: Logique en informatique [cs.LO]

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⟩