On Finitely Recursive Programs

Disjunctive finitary programs are a class of logic programs admitting function symbols and hence infinite domains. They have very good computational properties, for example ground queries are decidable while in the general case the stable model semantics is Ð1 1-hard. In this paper the authors prove that a larger class of programs, called finitely recursive programs, preserves most of the good properties of finitary programs under the stable model semantics, namely: Finitely recursive programs enjoy a compactness property; inconsistency checking and skeptical reasoning are semidecidable; skeptical resolution is complete for normal finitely recursive programs. Moreover, they show how to check inconsistency and answer skeptical queries using finite subsets of the ground program instantiation.