On the Expressibility of Stable Logic Programming

Abstract

Schlipf [Sch95] proved that Stable Logic Programming (SLP) solves all NP decision problems. We extend Schlipf’s result to prove that SLP solves all search problems in the class NP. Moreover, we do this in a uniform way as defined in [MT99]. Specifically, we show that there is a single DATALOG⌝ program P _Trg such that given any Turing machine M, any polynomial p with non-negative integer coefficients and any input σ of size n over a fixed alphabet ∑, there is an extensional database edb _M,p,σ such that there is a one-to-one correspondence between the stable models of edb _M,p,σ ∪ P_Trg and the accepting computations of the machine M that reach the final state in at most p(n) steps. Moreover, edb _M,p,σ can be computed in polynomial time from p, σ and the description of M and the decoding of such accepting computations from its corresponding stable model of edb _M,p,σ ∪ P _Trg can be computed in linear time. A similar statement holds for Default Logic with respect to∑^stackP _stack2-search problems.

We also show that there is single program Meta which is a metainterpreter for SLP programs. That is, for any program Q, there there is an encoding of Q as an extensional data base edb _Q such that the stable models of Meta ∪ edb _Q are in one-to-one correspondence with the stable models of Q.