Unification modulo Lists with Reverse as Solving Simple Sets of Word Equations
Siva Anantharaman, Peter Hibbs, Paliath Narendran, Michaël Rusinowitch · INRIA a CCSD electronic archive server · 2019
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.