Reasoning About Recursively Defined Data Structures
- 1 July 1980
- journal article
- Published by Association for Computing Machinery (ACM) in Journal of the ACM
- Vol. 27 (3) , 403-411
- https://doi.org/10.1145/322203.322204
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.)Keywords
This publication has 4 references indexed in Scilit:
- Variations on the Common Subexpression ProblemJournal of the ACM, 1980
- Fast Decision Procedures Based on Congruence ClosureJournal of the ACM, 1980
- Simplification by Cooperating Decision ProceduresACM Transactions on Programming Languages and Systems, 1979
- Abstract data types and software validationCommunications of the ACM, 1978