Skip to Main content Skip to Navigation
Conference papers

Unification modulo Lists with Reverse, Relation with Certain Word Equations

Siva Anantharaman 1, 2 Peter Hibbs 3 Paliath Narendran 4 Michaël Rusinowitch 5
1 LIFO - Laboratoire d'Informatique Fondamentale d'Orléans
2 INSA CVL - Institut National des Sciences Appliquées - Centre Val de Loire
3 SUNY - State University of New York
4 University at Albany [SUNY]
5 PESTO - Proof techniques for security protocols
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : 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.
Keywords : Lists Strings(Words) Unification Formal Verification Complexity.
Document type :
Conference papers
Complete list of metadatas

Cited literature [26 references]  Display  Hide  Download
https://hal.archives-ouvertes.fr/hal-02123709
Contributor : Siva Anantharaman <>
Submitted on : Wednesday, July 8, 2020 - 4:51:52 PM
Last modification on : Thursday, July 9, 2020 - 12:39:21 PM

File

Vignette du document
Cade27-Final.pdf
Files produced by the author(s)

Identifiers

Collections

MSL-THESE | INSA-GROUPE | MSL | UNIV-ORLEANS | LORIA | CNRS | UNIV-LORRAINE | INRIA | LORIA-FM | INSA-CVL

Citation

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⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

129

Files downloads

27

Données de recherche