Reasoning with infinite stable models

Abstract

The existing proof-theoretic and software tools for nonmonotonic reasoning can only handle finite domains. In this paper we introduce a class of normal logic programs, called finitary programs, whose domain may be infinite, and such that credulous and skeptical entailment under the stable model semantics are computable. Finitary programs— that are characterized by two conditions on their dependency graph—are computationally complete (they can simulate arbitrary Turing machines). Further results include a compactness theorem and the proof that the two conditions defining finitary programs are, in some sense, “minimal”. The existing methods for automated nonmonotonic reasoning are either complete for finitary programs, or can be easily extended to cover them.