Index sets for Finite Normal Predicate Logic Programs

TL;DR

This paper establishes a correspondence between stable models of finite predicate logic programs and paths through recursive trees, enabling complexity analysis of index sets for various program properties.

Contribution

It introduces recursive functions that relate stable models to tree paths, reducing the complexity analysis to well-studied problems in recursive tree index sets.

Findings

Determined the complexity of index sets for properties like no stable models and finitely many stable models.

Established degree-preserving correspondences between stable models and infinite paths in recursive trees.

Reduced complexity analysis of logic programs to primitive recursive tree index set problems.

Abstract

<Q>_e is the effective list of all finite predicate logic programs. <T_e> is the list of recursive trees. We modify constructions of Marek, Nerode, and Remmel [25] to construct recursive functions f and g such that for all indices e, (i) there is a one-to-one degree preserving correspondence between the set of stable models of Q_e and the set of infinite paths through T_{f(e)} and (ii) there is a one-to-one degree preserving correspondence between the set of infinite paths through T_e and the set of stable models of Q_{g(e)}. We use these two recursive functions to reduce the problem of finding the complexity of the index set I_P for various properties P of normal finite predicate logic programs to the problem of computing index sets for primitive recursive trees for which there is a large variety of results [6], [8], [16], [17], [18], [19]. We use our correspondences to determine the complexity of the index sets of all programs and of certain special classes of finite predicate logic programs of properties such as (i) having no stable models, (ii) having at least one stable model, (iii) having exactly c stable models for any given positive integer c, (iv) having only finitely many stable models, or (vi) having infinitely many stable models.