Skip to Main content Skip to Navigation
New interface
Conference papers

Rule-Based Unification in Combined Theories and the Finite Variant Property

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 :
Conference papers
Complete list of metadata

Cited literature [20 references]  Display  Hide  Download
Contributor : Christophe Ringeissen Connect in order to contact the contributor
Submitted on : Tuesday, April 2, 2019 - 2:47:15 PM
Last modification on : Friday, November 18, 2022 - 9:24:34 AM
Long-term archiving on: : Wednesday, July 3, 2019 - 3:12:05 PM


Files produced by the author(s)




Ajay K. Eeralla, Serdar Erbatur, Andrew M. Marshall, Christophe Ringeissen. Rule-Based Unification in Combined Theories and the Finite Variant Property. LATA 2019 - 13th International Conference on Language and Automata Theory and Applications, Mar 2019, Saint-Petersbourg, Russia. pp.356--367, ⟨10.1007/978-3-030-13435-8_26⟩. ⟨hal-01988419⟩



Record views


Files downloads