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

International audienceWe 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