The paper presents a calculus based on resolution for credulous reasoning in Answer Set Programming. The new approach allows a top-down and goal directed resolution, in the same spirit as traditional SLD-resolution. The proposed credulous resolution can be used in query-answering with nonground queries and with non-ground, and possibly infinite, programs. Soundness and completeness results for the resolution procedure are proved for large classes of logic programs. The resolution procedure is also extended to handle some traditional syntactic extensions used in Answer Set Programming, such as choice rules and constraints. The paper also describes an initial implementation of a system for credulous reasoning in Answer Set Programming.
Piero A. Bonatti, Enrico Pontelli, Tran Cao Son