How complicated is the set of stable models of a recursive logic program?

AbstractGelfond and Lifschitz (1988) proposed the notion of a stable model of a logic program. We establish that the set of all stable models in a Herbrand universe of a recursive logic program is, up to recursive renaming, the set of all infinite paths of a recursive, countably branching tree, and conversely. As a consequence, the problem, given a recursive logic program, of determining whether it has at least one stable model, is Σ11-complete. Due to the equivalences established in the authors' previous nonmonotone rule systems papers (Marek, Nerode and Remmel (1990)), this applies equally to truth maintenance systems and default logics