On finitely recursive programs

Finitary programs are a class of logic programs admitting functions symbols and hence infinite domains. In this paper we 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: (i) finitely recursive programs enjoy a compactness property; (ii) inconsistency check and skeptical reasoning are semidecidable; (iii) skeptical resolution is complete. Moreover, we show how to check inconsistency and answer skeptical queries using finite subsets of the ground program instantiation.