Abduction is a form of inference that supports hypothetical reasoning and has been applied to a number of domains, such as diagnosis, planning, protocol veri cation. Abductive Logic Programming (ALP) is the integration of abduction in logic programming. Usually, the operational semantics of an ALP language is de ned 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 e cient solution, but prevents de ned 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 di erent 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.
cause. Besides diagnosis, abductive reasoning has been applied to a number of
applications, like planning [
Abductive Logic Programming (ALP) [
A number of researchers have become interested in abductive reasoning
because it deals in a simple and sound way with negation [
ALP has also been integrated with Constraint Logic Programming [
Kowalski et al. [
The rst works on the implementation of abductive reasoning in CHR [13{16] implemented directly the integrity constraints into CHR rules: in a sense, CHR becomes also the language for writing integrity constraints. Thus, the user can write rules such as
p ^ q ! r;
where p and q are abducible predicates and r can be either an abducible or
a de ned predicate. The interest of a CHR implementation is not only
theoretical: thanks to the tight integration of CHR in the host language (which is
often Prolog), those proof-procedures can seamlessly access built-in constructs
and constraint solvers. This means that they have access to the innumerable
libraries written in Prolog, and they can even recurse through external predicates:
the abductive program can invoke Prolog predicates, and also meta-predicates
(e.g., findall, minimize, . . . ), which can in their turn request the abduction
of atoms, etc. A proof-procedure written in CHR bene ts immediately from all
the improvements of CHR engines, as recently happened with the Leuven CHR
implementation [
However, a rule with a de ned predicate in the antecedent is not allowed: these languages sacri ce negation by default on the altar of e ciency, which is a sensible thing to do in some applications, but it is not in others.
The SCIFF proof-procedure [
SCIFF has been continuously developed and improved in the past few years, and now it is smoothly integrated in graphical interfaces, semantic web applications; it is considerably faster, more robust, and provides more features.
In this paper, we show the implementation in CHR of the abductive proofprocedure SCIFF, and we report about its recent improvements.
The rest of the paper is organised as follows. We rst describe the SCIFF abductive framework in Section 2. After some preliminaries on CHR (Section 3), we present the implementation of SCIFF in CHR (Section 4). Discussion of related work (Section 5) and conclusions (Section 6) follow. 2
Abductive Logic Programming is a family of programming languages that integrate abductive reasoning into logic programming. An ALP is a logic program, consisting of a set of clauses, that can contain in the body some distinguished predicates, belonging to a set A and called abducibles, (that will be shown in the following in boldface). The aim is nding a set of abducibles A that, together with the knowledge base, is an explanation for a given known e ect (also called goal G):
KB [ j= G:
KB [
j= IC: headache headache headache
u: migraine: meningitis: and the abductive system will return one of the three explanations.
SCIFF [
u ! temp(T ); T < 39 saying that the explanation u is acceptable only if the temperature of the patient is less than 39oC. The computed answer includes in general three elements: a substitution for the variables in the goal (as usual in Prolog), the constraint store (as in CLP), and the set of abduced literals.
SCIFF was originally developed for the veri cation of interaction in
multiagent systems [
Constraint Handling Rules [
The main intended use for CHR is to write constraint solvers, or to extend existing ones. However, the computational model of CHR presents features that make it a useful tool for the implementation of the SCIFF proof-procedure.
There are three types of CHRs: simpli cation, propagation and simpagation.
H1; : : : ; Hi () G1; : : : ; Gj jB1; : : : ; Bk (1) with i > 0, j 0, k 0 and where the multi-head H1; : : : ; Hi is a nonempty sequence of CHR constraints, the guard G1; : : : ; Gj is a sequence of built-in constraints, and the body B1; : : : ; Bk is a sequence of built-in and CHR constraints.
Declaratively, a simpli cation rule states that, if the guard is true, then the left-hand-side and the right-hand-side are equivalent.
Operationally, when constraint instances H1; : : : ; Hi in the head are in the store and the guard G1; : : : ; Gj is true, they are replaced by constraints B1; : : : ; Bk in the body.
H1; : : : ; Hi =) G1; : : : ; Gj jB1; : : : ; Bk (2) where the symbols have the same meaning of those in the simpli cation rules (1).
Declaratively, a propagation rule is an implication, provided that the guard is true. Operationally, when the constraints in the head are in the store, and the guard is true, the constraints in the body are added to the store.
H1; : : : ; HlnHl+1; : : : ; Hi () G1; : : : ; Gj jB1; : : : ; Bk where l > 0 and the other symbols have the same meaning and constraints of those of simpli cation CHRs (1).
Declaratively, the rule of Eq. (3) is equivalent to
H1; : : : ; Hl; Hl+1; : : : ; Hi () G1; : : : ; Gj jB1; : : : ; Bk; H1; : : : ; Hl (4) Operationally, when the constraints in the head are in the store and the guard is true, H1; : : : ; Hl remain in the store, and Hl+1; : : : ; Hi are replaced by B1; : : : ; Bk.
For example, the constraint can be implemented in CHR by giving its base properties, namely the following rules: Simpagation CHRs. Simpagation rules have the form (3) (5) (6) (7) A A
A B; B B; B
A , true C ) A A , A = B
C where the symbol '=' stands for uni cation. The CHR engine rewrites the constraints in the store occurring as in the left-hand-side of the rules; for example, if the constraints X Y , Y X are in the store, they are removed from the store and the variables X and Y are uni ed, as prescribed by rule 6. Note that on the left-hand-side of a CHR rule only constraints de ned with CHR can appear: while the right-hand-side can contain any Prolog predicate (including CLP(FD) constraints, uni cations, etc.), these elements cannot appear on the left-hand-side. 4
Implementation of the S CIFF proof-procedure One of the features obtained through a CHR implementation (avoiding metainterpretation) is that the resolvent of the proof is directly represented as the Prolog resolvent. This allows us to exploit the Prolog stack for depth- rst exploration of the tree of states. More importantly, this means that we extensively reuse the Prolog machinery, and that built-in predicates in the host Prolog system can be called from the user's Abductive Logic Programs. We remark again that this feature comes for free together with the CHR implementation, and is not easily available in metainterpreter-based implementations of abductive proof-procedures.
In the same way, the constraint store of the constrained abductive
proofprocedure3 is represented as the union of the CLP constraint stores. For the
implementation of the proof-procedure, we used the CLP(FD) and CLP(B)
libraries, available both on SICStus [
CHR-based solver on nite and in nite domains, and we de ned an ad-hoc solver
for rei ed uni cation. Recently, the interface between SCIFF and the constraint
solver has been re-engineered, and now it allows the developer to adopt any
constraint solver that implements a given interface. In this way, the user can choose
for each application which solver he/she wants to use; moreover, new solvers
can be added with very limited e ort. For example, the constraint solver on the
reals, CLP(R) [
To the best of our knowledge, the other abductive proof-procedures
implemented in CHR map abducibles to CHR constraints. Integrity constraints,
instead, are often represented as CHR rules (typically, propagation rules) [
SCIFF was developed following a di erent idea: we wanted increased
exibility in our language, while retaining the features that come for free with the CHR
implementation. We rst de ned the declarative and operational semantics of
SCIFF as extensions of the IFF [
In the following, we rst show some examples of transitions; the interested
reader can nd the complete list of transitions in a previous publication [
Examples of transitions
a(Y ) ^ p(Z) ^ Y > Z ! r(Z) transition propagation generates the following implication (that we call Partially Solved Integrity Constraint or PSIC for short):
X = Y ^ p(Z) ^ Y > Z ! r(Z) (8) Now, a transition case analysis generates two nodes of an OR-tree: in the rst we consider the case X = Y , so the previous implication is transformed into p(Z) ^ X > Z ! r(Z); in the second node, we consider the case that X 6= Y , and in this case the implication (8) is already satis ed.
Suppose we choose the rst node, and that the knowledge base contains the de nition of predicate p(Z), e.g., as a fact p(1). Transition unfolding generates the following implication:
X > 1 ! r(1) Now, case analysis is again applied to the implication: in the rst node we consider the case X > 1, while in the second X 1. In the rst case, the goal r(1) is invoked.
These are just some examples of the transitions. SCIFF contains transitions for handling correctly the various items (abducibles, expectations, happened events, CLP constraints, negation by default, explicit negation, etc.) in the SCIFF language. 4.2
CHR implementation The implementation of the transitions in CHR follows very closely the operational semantics. The various types of data are mapped to CHR constraints, while the transitions are mapped into CHR rules. For example, abducibles are represented as abd(X); this means that abducibles can be directly used in the knowledge base, and CHR will take care of all the machinery necessary to abduce a new literal and propagate its consequences. For example, the clause can be written as
g(X) : a(X); b: g(X) :- abd(a(X)), b.
a(X) ^ p(Y ) ! r(Z) _ q(Z) is mapped to the CHR constraint
psic([abd(a(X)),p(Y)],(r(Z);q(Z))):
As a rst attempt, the propagation transition (together with case analysis) can be implemented via the CHR rule abd(X), psic([abd(Y)|Rest],Head)
==>
copy(psic([abd(Y)|Rest],Head),psic([abd(Y1)|Rest1],Head1)),
reif_unify(X,Y1,B),
(B#=1, psic(Rest1,Head1) ; B#=0).
(9)
where copy performs a renaming of an atom (which also considers the various
types of quanti cation in the SCIFF [
reif_unify is a CHR constraint that declaratively imposes that either B = 1 and the rst two arguments unify, or B = 0 and the two atoms do not unify; in logics, reif_unify(X,Y,B) is true i
X = Y $ B = 1:
Note that some of the details are taken care of directly by CHR: if we have a set of abducibles and a set of PSICs we do not have to remember explicitly which PSICs have been tried with which abducibles (in order to avoid loops), as CHR itself does this work.
Note also that propagation is attempted only with the rst element of the partially solved integrity constraint's antecedent, but this does not impact on what integrity constraints will be completely solved. For instance, given the integrity constraint a; b ! c, if b and a are abduced in sequence, b will not be propagated as soon as it is abduced, but only after a has been abduced and propagated, and the partially solved integrity constraint b ! c has been added to the constraint store; in the end, c will be abduced anyway. In this way, we ensure that each atom is propagated only once with each integrity constraint, without a need to keep track of previous propagations.
A number of improvements can be done to rule (9). First of all, CHR uses e cient indexing and hash tables to avoid checking all the possible pairs of CHR constraints. Sadly, rule (9) does not exploit such features of CHR. Note that the constraints in the antecedent of the propagation CHR do not share any variable, thus the CHR engine has to try each possible pair of constraints of types abd and psic, while, intuitively, one should try only those pairs whose arguments may unify. A rst idea would be to rewrite the transition as: abd(X), psic([abd(X)|Rest],Head)
==> ... which would use CHR hash tables much more e ciently, but it would propagate only when the arguments are already ground or bound to the same term. This would be a very lazy propagation, that does not exploit the rei ed uni cation algorithm.
However, since abducibles are atoms, they always have a main functor, thus the argument of abd is always a term, which can contain variables, but it cannot be a variable itself. It is sensible to exploit the main functor for improving the selection of candidates. We represent each abducible as a CHR constraint with two arguments, where the rst argument contains a ground term used to improve the hashing: in the current implementation, it is a list containing the main functor and its arity. The code for abducing an atom X is then: abd(X) :- functor(X,F,A), abd([F,A],X).
Now, the propagation transition can be implemented with the CHR propagation rule: abd(F,X), psic([abd(F,Y)|Rest],Head) ==> fn_ok(X,Y) | copy(psic([abd(Y)|Rest],Head),psic([abd(Y1)|Rest1],Head1)), (10) reif_unify(X,Y1,B), (B#=1, psic(Rest1,Head1) ; B#=0). i.e., only those pairs with identical rst argument (i.e., abducibles that share the same functor and arity) are tried. fn_ok is a predicate that checks if the two arguments can possibly unify, and is also used for improving e ciency.
Many of the transitions of SCIFF open a choice point, as we can see from the example of Eq. (10). However, in case reif_unify immediately yields 0 or 1, there is no point in opening a choice point. Otherwise, one could delay the disjunction, in order to open choice points as late as possible, hoping that other transitions might constrain the value of the B variable, possibly making it ground. In other words, it would be more desirable to delay as much as possible the non-deterministic transitions (those opening choice points), while expediting the deterministic ones (those that do not open choice points). One reason is that the deterministic may fail, and in this case the choice points opened by nondeterministic choices would be useless.
In order to implement the delay mechanism, we de ned a CHR constraint 'nondeterministic' that holds, as argument, a non-deterministic goal. In the previous example, the propagation transition is actually rewritten as abd(F,X), psic([abd(F,Y)|Rest],Head) ==> fn_ok(X,Y) | copy(psic([abd(Y)|Rest],Head),psic([abd(RenY)|RenRest],RenHead)), reif_unify(X,RenY,B), (B == 1 -> psic(RenRest,RenHead) ;
B == 0 -> true ; nondeterministic((B#=1, psic(RenRest,RenHead)) ; B#=0)). i.e., we check if rei ed uni cation imposed a value on the boolean variable B, and we open a choice point only in case it did not. The choice point is not actually opened immediately, but it is declared in a CHR constraint.
Then, we de ned a set of CHRs for dealing with nondeterministic
constraints. We alternate a deterministic and a non-deterministic phase: initially, in
the derivation, only deterministic transitions can be activated. Later, when the
xed point of the deterministic ones is reached, one non-deterministic transition
can be applied, and we return to the deterministic phase. In CHR:
switch2det @ phase(nondeterministic), nondeterministic(G) <=>
call(G),
phase(deterministic).
switch2nondet @ phase(deterministic) <=> phase(nondeterministic).
where rule switch2nondet should be one of the last rules to be tried.
Transition Unfolding. Di erently from HYPROLOG [
This might pose problems of termination: if the unfolded predicate is recursive, there exists an in nite branch in the derivation. For example, consider the IC: a(List); member(T erm; List) ! b(T erm) (11) with the knowledge base: member(X; [XjT ]): member(X; [Y jT ]) : member(X; T ): g : a([1; 2; 3]): Intuitively, the goal g is true provided that we abduce a([1; 2; 3]) and b(1), b(2), b(3). However, if we unfold predicate member in the IC (11) before the atom a([1; 2; 3]) was abduced, the unfolding generates an in nite number of implications. For this reason, early versions of SCIFF delay the unfolding after the other transitions, in the hope of binding some of the variables. In this particular example, if member is unfolded only after a([1; 2; 3]) is abduced, the number of implications generated is equal to the number of elements in the list L, which is nite.
However, in other cases de ned predicates provide just the value of a parameter, in this example, a deadline: start(a; Ta) ^ deadline(D) ! end(b; Tb) ^ Tb The knowledge base contains a simple fact deadline(5) stating that the deadline is 5 time units. In this case, if the unfolding of deadline is postponed after propagation of the start(a; Ta) event, it is repeated as many times as the number of start atoms that will be abduced, which might be a big number. For this reason, recent versions of SCIFF unfold eagerly the predicates de ned only by facts, and lazily the other predicates.
Results. The e ciency of SCIFF has greatly improved with respect to earlier
versions [
Experiment Auction Protocol Block World AlLoWS Feeble conformance AlLoWS non-conformant
The aim of these experiments is not to compete with other abductive
proofprocedures, but to show the improvements obtained taking into consideration the
features of CHR. The version 2011 features improved hashing, eager unfolding,
and other minor improvements. The experiments are real-life applications that
we developed in SCIFF: the proof of conformance of agents to an auction
protocol, planning in the abductive event calculus, and AlLoWS [
The SCIFF abductive framework is derived from the IFF proof procedure [
Other proof-procedures deal with constraints; in particular we mention ACLP
[
Some conspicuous work has been done with the integration of the IFF
proofprocedure with constraints [
All of these proof-procedures are implemented as Prolog meta-interpreters. However, we believe that a CHR implementation has features that a metainterpreted version cannot have, as we explained in the introduction.
Abdennadher and Christiansen [
In this paper, we have presented the implementation of an abductive
proofprocedure in CHR. We believe that the use of CHR in writing abductive
proofprocedures has several advantages, compared to traditional approaches based
on meta-interpretation. The rst advantage is that SCIFF bene ts immediately
from new implementations and improvements of CHR engines [
An interesting extension of this work would be to integrate the two main ideas for implementing abduction in CHR in a unique framework. Each of the ideas have their own pros and cons: HYPROLOG, that implements integrity constraints as CHR rules, has less overhead, while SCIFF, that maps integrity constraints into CHR constraints, is able to deal with default negation and is provably sound and complete. We are currently studying the idea of selecting syntactically the integrity constraints in an ALP in a preprocessing phase, and implementing each in the most e cient possible way, i.e., as CHR rules, whenever possible, or as CHR constraints when they contain de ned predicates or CLP(FD) constraints.
Concerning con rmation, there are many possible extensions of this work, which we intend to pursue in the future. For instance, it would be worthwhile to let the user impose the failure of a branch of the reasoning tree, regardless of the con rmation or discon rmation of the hypotheses made in the branch, in order to explore branches that the user nds more promising. We also intend to support a breadth- rst exploration of the computation tree, as an alternative to the depth- rst exploration of the current implementation. Besides, we believe that the formal framework would bene t from the introduction of a formalism to express priorities among the possible alternative hypotheses, in a given state of the computation.
Another direction of improvement could be towards better computational
performance, possibly exploiting alternative e cient CHR implementations, such
as the one proposed by Wolf [
This work has been supported by the European Commission within the e-Policy project (n. 288147).