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

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

Ajay Kumar Eeralla, Serdar Erbatur, Andrew M. Marshall, and Christophe Ringeissen. Rule-Based Unification in Combined Theories and the Finite Variant Property. In 13th International Conference on Language and Automata Theory and Applications (LATA'19), pp. 356–367, Lecture Notes in Computer Science 11417, Springer, 2019.
doi:10.1007/978-3-030-13435-8_26

Download

[PDF] [HTML]

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.

BibTeX

@inproceedings{EEMR-lata19,
  author =	 {Ajay Kumar Eeralla and Serdar Erbatur and Andrew
                  M. Marshall and Christophe Ringeissen},
  title =	 {Rule-Based Unification in Combined Theories and the
                  Finite Variant Property},
  booktitle =	 {13th International Conference on Language and
                  Automata Theory and Applications ({LATA}'19)},
  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.},
  pages =	 {356--367},
  year =	 2019,
  doi =		 {10.1007/978-3-030-13435-8\_26},
  series =	 {Lecture Notes in Computer Science},
  volume =	 11417,
  publisher =	 {Springer},
  doi =		 {10.1007/978-3-030-13435-8_26},
                  ={https://hal.inria.fr/hal-01988419/file/combi-fc.pdf},
}