Unification dans des mélanges non-disjoints avec des théories fermées en avant
Ajay Kumar Eeralla, Serdar Erbatur, Andrew M. Marshall, Christophe Ringeissen · HAL (Le Centre pour la Communication Scientifique Directe) · 2019
We investigate the unification problemin theories defined by rewrite systems which are both convergent andforward-closed. These theories are also known in the context ofprotocol analysis as theories with the finite variant property andadmit a variant-based unification algorithm. In this paper, wepresent a new rule-based unification algorithm which can be seen as analternative to the variant-based approach. In addition, we defineforward-closed combination to capture the union of a forward-closedconvergent rewrite system with another theory, such as theAssociativity-Commutativity, whose function symbols may occur inright-hand sides of the rewrite system. Finally, we present acombination algorithm for this particular class of non-disjoint unionsof theories.