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

4Citations
Citations of this article
1Readers
Mendeley users who have this article in their library.
Get full text

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.

Cite

CITATION STYLE

APA

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

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free