Unification in Non-Disjoint Combinations with Forward-Closed Theories

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.
Document type :
Reports
Complete list of metadatas

https://hal.inria.fr/hal-02006179
Contributor : Christophe Ringeissen <>
Submitted on : Monday, February 4, 2019 - 2:33:48 PM
Last modification on : Wednesday, April 3, 2019 - 1:22:59 AM
Long-term archiving on : Sunday, May 5, 2019 - 3:19:41 PM

File

RR-9252.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02006179, version 1

Citation

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

Share

Metrics

Record views

57

Files downloads

82