Locally determined logic programs and recursive stable models (Q1430287)

The logic program {\textit{P}} is a finite set of clauses of the form \(C = p \leftarrow q_{1},\dots ,q_{n},\neg r_{1},\dots ,\neg r_{m}\), where {\textit{p}}\(,{q_{1}},\dots , {q_{n}},{r_{1}},\dots ,{r_{m}}\) are atomic formulas possibly with variables in some first-order logic. The authors consider Herbrand's type models of logic programs and recursive logic programs connected with Gödel numbering of the elements of the Herbrand base. Theorem 1. If {\textit{T}} is a highly recursive tree contained in \(\omega^{\omega}\), then there exists an effectively locally determined recursive logic program {\textit{P}} such that there is an effective one-to-one degree preserving correspondence between the set of infinite paths through {\textit{T}} and the set of all stable models of the program {\textit{P}}. Theorem 2. If {\textit{P}} is a recursive logic program which has witnesses with effective delay and has at least one stable model, then the lexicographically least stable model of {\textit{P}} is recursive. The authors define a polynomial-time version of effectively locally determined recursive logic programs and recursive logic programs with effective witnesses which ensure that a logic program {\textit{P}} has models which are NP, EXPTIME, etc. They characterize the set of stable models of locally determined logic programs.