Skip to Main content Skip to Navigation

Unification in Non-Disjoint Combinations with Forward-Closed Theories

Abstract : We investigate the unification problem in theories defined by rewrite systems which are both convergent and forward-closed. These theories are also known in the context of protocol analysis as theories with the finite variant property and admit a variant-based unification algorithm. In this paper, we present a new rule-based unification algorithm which can be seen as an alternative to the variant-based approach. In addition, we define forward-closed combination to capture the union of a forward-closed convergent rewrite system with another theory, such as the Associativity-Commutativity, whose function symbols may occur in right-hand sides of the rewrite system. Finally, we present a combination algorithm for this particular class of non-disjoint unions of theories.
Document type :
Complete list of metadata

Cited literature [27 references]  Display  Hide  Download
Contributor : Christophe Ringeissen Connect in order to contact the contributor
Submitted on : Monday, February 4, 2019 - 2:33:48 PM
Last modification on : Saturday, October 16, 2021 - 11:26:10 AM
Long-term archiving on: : Sunday, May 5, 2019 - 3:19:41 PM


Files produced by the author(s)


  • HAL Id : hal-02006179, version 1


Ajay Eeralla, Serdar Erbatur, Andrew Marshall, Christophe Ringeissen. Unification in Non-Disjoint Combinations with Forward-Closed Theories. [Research Report] RR-9252, Inria Nancy - Grand Est. 2019. ⟨hal-02006179⟩



Record views


Files downloads