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