Credulous Resolution for Answer Set Programming

Piero Bonatti, Enrico Pontelli, Tran Cao Son

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 non-ground 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.

Subjects: 3.3 Nonmonotonic Reasoning; 8. Enabling Technologies

Submitted: Apr 11, 2008

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.