BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CS-TR-78-678
       ENTRY:: June 22, 1995
ORGANIZATION:: Stanford University, Department of Computer Science
       TITLE:: Reasoning about recursively defined data structures
        TYPE:: Technical Report
      AUTHOR:: Oppen, Derek C.
        DATE:: July 1978
       PAGES:: 15
    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.
       NOTES:: [Adminitrivia V1/Prg/19950622]
         END:: STAN//CS-TR-78-678