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.
CITATION STYLE
Eeralla, A. K., Erbatur, S., Marshall, A. M., & Ringeissen, C. (2019). Rule-Based Unification in Combined Theories and the Finite Variant Property. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11417 LNCS, pp. 356–367). Springer Verlag. https://doi.org/10.1007/978-3-030-13435-8_26
Mendeley helps you to discover research relevant for your work.