Report Number: CS-TR-78-678
Institution: Stanford University, Department of Computer Science
Title: Reasoning about recursively defined data structures
Author: Oppen, Derek C.
Date: July 1978
Abstract: A decision algorithm 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.
http://i.stanford.edu/pub/cstr/reports/cs/tr/78/678/CS-TR-78-678.pdf