Reasoning About Recursively Defined Data Structures

Abstract

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.)