Skip to Main content Skip to Navigation
Conference papers

Unification modulo Lists with Reverse, Relation with Certain Word Equations

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

Cited literature [26 references]  Display  Hide  Download
Contributor : Siva Anantharaman <>
Submitted on : Wednesday, July 8, 2020 - 4:51:52 PM
Last modification on : Thursday, July 9, 2020 - 12:39:21 PM
Long-term archiving on: : Monday, November 30, 2020 - 3:39:05 PM


Files produced by the author(s)



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⟩



Record views


Files downloads


Données de recherche

doi: web.