Hostname: page-component-78c5997874-94fs2 Total loading time: 0 Render date: 2024-11-20T05:06:10.407Z Has data issue: false hasContentIssue false

On the expressibility of stable logic programming

Published online by Cambridge University Press:  31 July 2003

VICTOR W. MAREK
Affiliation:
Department of Computer Science, University of Kentucky, Lexington, KY 40506, USA (e-mail: [email protected])
JEFFREY B. REMMEL
Affiliation:
Department of Mathematics, University of California, San Diego, La Jolla, CA 92093, USA (e-mail: [email protected])

Abstract

Schlipf (1995) proved that Stable Logic Programming (SLP) solves all $\mathit{NP}$ decision problems. We extend Schlipf's result to prove that SLP solves all search problems in the class $\mathit{NP}$. Moreover, we do this in a uniform way as defined in Marek and Truszczyński (1991). Specifically, we show that there is a single $\mathrm{DATALOG}^{\neg}$ program $P_{\mathit{Trg}}$ such that given any Turing machine $M$, any polynomial $p$ with non-negative integer coefficients and any input $\sigma$ of size $n$ over a fixed alphabet $\Sigma$, there is an extensional database $\mathit{edb}_{M,p,\sigma}$ such that there is a one-to-one correspondence between the stable models of $\mathit{edb}_{M,p,\sigma} \cup P_{\mathit{Trg}}$ and the accepting computations of the machine $M$ that reach the final state in at most $p(n)$ steps. Moreover, $\mathit{edb}_{M,p,\sigma}$ can be computed in polynomial time from $p$, $\sigma$ and the description of $M$ and the decoding of such accepting computations from its corresponding stable model of $\mathit{edb}_{M,p,\sigma} \cup P_{\mathit{Trg}}$ can be computed in linear time. A similar statement holds for Default Logic with respect to $\Sigma_2^\mathrm{P}$-search problems.The proof of this result involves additional technical complications and will be a subject of another publication.

Type
Regular Papers
Copyright
© 2003 Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)