Thumbnail
Access Restriction
Subscribed

Author Venkataraman, K. N.
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Copyright Year ©1987
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Abstract This paper is concerned with the question of the $\textit{decidability}$ and the $\textit{complexity}$ of the decision problem for certain fragments of the theory of free term algebras. The existential fragment of the theory of term algebras is shown to be decidable through the presentation of a nondeterministic algorithm, which, given a quantifier-free formula $\textit{P},$ constructs a solution for $\textit{P}$ if it has one and indicates failure if there are no solutions. It is shown that the decision problem is in NP by proving that, if a quantifier-free formula $\textit{P}$ has a solution, then there is one that can be represented as a dag in space at most cubic in the length of $\textit{P}.$ The decision problem is shown to be complete for NP by reducing 3-SAT to that problem. Thus it is established that the existential fragment of the theory of pure list structures in the language of NIL, CONS, CAR, CDR, =, ≤ (subexpression) is NP-complete. It is further shown that even a slightly more expressive fragment of the theory of term algebras, the one that allows bounded universal quantifiers, is undecidable.
ISSN 00045411
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 1987-04-01
Publisher Place New York
e-ISSN 1557735X
Journal Journal of the ACM (JACM)
Volume Number 34
Issue Number 2
Page Count 19
Starting Page 492
Ending Page 510


Open content in new tab

   Open content in new tab
Source: ACM Digital Library