### Decidability of the purely existential fragment of the theory of term algebrasDecidability of the purely existential fragment of the theory of term algebras

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

Source: ACM Digital Library