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.