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.

The CHR-based Implementation of the SCIFF Abductive System

ALBERTI, Marco;GAVANELLI, Marco;LAMMA, Evelina
2011

Abstract

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.
2011
computational logic; Abduction; proof procedure
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in SFERA sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11392/2248612
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? ND
social impact