Reasoning About Recursively Defined Data Structures
Derek C. Oppen · Journal of the ACM · 1980
A decision procedure is given for the quantifier-free theory of recursively defined data structures which, for a conjunction of length n, decides its satisfiability in time linear in n.The first-order theory of recursively defined data structures, in particular the first-order theory of LISP list structure (the theory of cons, car, and cdr), is shown to be decidable but not elementary recursive.(This answers an open question posed by John McCarthy.)