The CHR-based Implementation of the SCIFF Abductive System

Abduction is a form of inference that supports hypothetical reasoning and has been applied to a number of domains, such as diagnosis, planning, protocol verication. Abductive Logic Programming (ALP) is the integration of abduction in logic programming. Usually, the operational semantics of an ALP language is dened as a proof procedure. The rst implementations of ALP proof-procedures were based on the meta-interpretation technique, which is exible but limits the use of the built-in predicates of logic programming systems. Another, more recent, approach exploits theoretical results on the similarity between abducibles and constraints. With this approach, which bears the advantage of an easy integration with built-in predicates and constraints, Constraint Handling Rules has been the language of choice for the implementation of abductive proof procedures. The rst CHR-based implementation mapped integrity constraints directly to CHR rules, which is an ecient solution, but prevents dened predicates from being in the body of integrity constraints and does not allow a sound treatment of negation by default. In this paper, we describe the CHR-based implementation of the SCIFF abductive proof-procedure, which follows a dierent approach. The SCIFF implementation maps integrity constraints to CHR constraints, and the transitions of the proof-procedure to CHR rules, making it possible to treat default negation, while retaining the other advantages of CHRbased implementations of ALP proof-procedures.