Unification modulo Lists with Reverse, Relation with Certain Word Equations - Modelisation Systemes Langages Accéder directement au contenu
Communication Dans Un Congrès Année : 2019

Unification modulo Lists with Reverse, Relation with Certain Word Equations

Résumé

Decision procedures for various list theories have been investigated in the literature with applications to automated verification. Here we show that the unifiability problem for some list theories with a \emph{reverse} operator is NP-complete. We also give a unifiability algorithm for the case where the theories are extended with a \emph{length} operator on lists.
Fichier principal
Vignette du fichier
Cade27-Final.pdf (182.88 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02123709 , version 1 (08-07-2020)

Identifiants

Citer

Siva Anantharaman, Peter Hibbs, Paliath Narendran, Michaël Rusinowitch. Unification modulo Lists with Reverse, Relation with Certain Word Equations. CADE-27 - The 27th International Conference on Automated Deduction, Association for Automated Reasoning (AAR), Aug 2019, Natal, Brazil. pp.1--17, ⟨10.1007/978-3-030-29436-6_1⟩. ⟨hal-02123709⟩
166 Consultations
118 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More