Peter Hibbs

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

2019 · INRIA a CCSD electronic archive server

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 …