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.)
No takes yet. Share an insight, caveat, or question.
Derek C. Oppen (1980) studied this question.
Synapse has enriched 5 related papers. Consider them for comparative context: