Unification modulo Lists with Reverse as Solving Simple Sets of Word Equations

Siva Anantharaman (1, 2) , Peter Hibbs (3) , Paliath Narendran (3) , Michael Rusinowitch (4)

1 LIFO - Laboratoire d'Informatique Fondamentale d'Orléans
2 INSA CVL - Institut National des Sciences Appliquées - Centre Val de Loire
3 University at Albany [SUNY]
4 LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications

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 reverse operator is NP-complete. We also give a unifiability algorithm for the case where the theories are extended with a length operator on lists.

Domaines: Informatique et langage [cs.CL]

Siva Anantharaman, Peter Hibbs, Paliath Narendran, Michael Rusinowitch. Unification modulo Lists with Reverse as Solving Simple Sets of Word Equations. 2019. ⟨hal-02123648v1⟩