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 metadatas

Cited literature [14 references]  Display  Hide  Download

https://hal.inria.fr/hal-01988419
Contributor : Christophe Ringeissen <>
Submitted on : Tuesday, April 2, 2019 - 2:47:15 PM
Last modification on : Tuesday, April 2, 2019 - 5:14:27 PM
Long-term archiving on : Wednesday, July 3, 2019 - 3:12:05 PM

File

combi-fc.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Ajay Eeralla, Serdar Erbatur, Andrew 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⟩

Share

Metrics

Record views

56

Files downloads

50