Unification in Non-Disjoint Combinations with Forward-Closed Theories - Archive ouverte HAL Access content directly
Reports (Research Report) Year : 2019

Unification in Non-Disjoint Combinations with Forward-Closed Theories

Unification dans des mélanges non-disjoints avec des théories fermées en avant

(1) , (2) , (3) , (4)
1
2
3
4

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.
On étudie le problème d’unification dans les théories définies par des systèmes de réécriture qui sont à la fois convergents et fermés en avant. Ces théories sont connues dans le contexte de l’analyse de protocoles de sécurité comme les théories ayant la propriété des variants finis et admettant de ce fait un algorithme d’unification à base de variants. Dans ce papier, on présente un nouvel algorithme d’unification à base de règles qui peut être vu comme une alternative à l’approche basée sur le calcul de variants. On étudie l’union d’un système de réécriture convergent et fermé en avant avec une autre théorie dont les symboles de fonction peuvent apparaître dans les membres droits du système de réécriture. Finalement, on présente un algorithme de combinaison pour cette classe particulière d’unions non-disjointes de théories.
Fichier principal
Vignette du fichier
RR-9252.pdf (885.74 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-02006179 , version 1 (04-02-2019)

Identifiers

  • HAL Id : hal-02006179 , version 1

Cite

Ajay K. Eeralla, Serdar Erbatur, Andrew M. Marshall, Christophe Ringeissen. Unification in Non-Disjoint Combinations with Forward-Closed Theories. [Research Report] RR-9252, Inria Nancy - Grand Est. 2019. ⟨hal-02006179⟩
76 View
67 Download

Share

Gmail Facebook Twitter LinkedIn More