The CHR-based Implementation of the SCIFF Abductive System Marco Alberti1, Marco Gavanelli2, and Evelina Lamma2 1 CENTRIA - DI/FCT - Universidade Nova de Lisboa Quinta da Torre - 2829-516 Caparica, Portugal 2 ENDIF - Universita` di Ferrara Via Saragat, 1 - 44100 Ferrara, Italy. [email protected],{marco.gavanelli|evelina.lamma}@unife.it Abstract. Abduction is a form of inference that supports hypothetical reasoning and has been applied to a number of domains, such as di- agnosis, planning, protocol verification. Abductive Logic Programming (ALP)istheintegrationofabductioninlogicprogramming.Usually,the operational semantics of an ALP language is defined as a proof proce- dure. The first implementations of ALP proof-procedures were based on the meta-interpretation technique, which is flexible 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 ad- vantage of an easy integration with built-in predicates and constraints, Constraint Handling Rules has been the language of choice for the im- plementationofabductiveproofprocedures.ThefirstCHR-basedimple- mentation mapped integrity constraints directly to CHR rules, which is an efficient solution, but prevents defined predicates from being in the body of integrity constraints and does not allow a sound treatment of negation by default. Inthispaper,wedescribetheCHR-basedimplementationoftheSCIFF abductiveproof-procedure,whichfollowsadifferentapproach.TheSCIFF 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 CHR- based implementations of ALP proof-procedures. 1 Introduction According to the philosopher Peirce [1], abductive reasoning is one of the ba- sic inferences a reasoning agent (and a human in particular) uses. It is a type of hypothetical reasoning associated with finding explanations for a given evi- dence. Its most classical application is diagnosis: we are given a symptom of a patient, or a wrong behaviour of a machine, plus a set of rules explaining which illnessesmightcausethesymptom/misbehaviour,andwehavetoguesstheright cause. Besides diagnosis, abductive reasoning has been applied to a number of applications, like planning [2], protocol verification [3], etc. Abductive Logic Programming (ALP) [4] is a language that embeds abduc- tive reasoning into logic programming. In ALP, we have a set of predicates that havenodefinition,andarecalledabducibles.Thetruthofsuchpredicatescannot be proven, but it can be assumed: the abductive derivation will provide in the computed answer the set of abduced hypotheses, together with the binding (the classical answer of Logic Programming languages). However, in typical applica- tions, not all combinations of assumptions make sense: some illnesses are to be excluded beforehand, depending e.g. on the sex of the patient. For this reason, in ALP the user can typically define a set of rules, called Integrity Constraints, that must be satisfied by the set of hypotheses. The operational semantics of anALPistypicallydefinedasaproof-procedure.Anumberofproof-procedures have been proposed in the past for performing abductive reasoning; they are typically implemented as Prolog meta-interpreters [5–8]. A number of researchers have become interested in abductive reasoning be- cause it deals in a simple and sound way with negation [9]. Literal not(a) is rewritten as an integrity constraint a → false, and then handled appropriately by the proof procedure. This type of negation is also called negation by default. ALP has also been integrated with Constraint Logic Programming [6,8,10], in order to use both abductive reasoning and constraint propagation. Kowalski et al. [11] studied the theoretical similarities between constraints and abducibles. Such similarity was later exploited for the implementation of abductive proof-procedures where abducibles are mapped to CLP constraints. For this purpose, a promising is Constraint Handling Rules (CHR) [12] a lan- guage designed to implement new constraints and constraint solvers in a simple and efficient way. ThefirstworksontheimplementationofabductivereasoninginCHR[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 defined predicate. The interest of a CHR implementation is not only theo- retical: 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 li- brarieswritteninProlog,andtheycanevenrecursethroughexternalpredicates: 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 benefits immediately from all the improvements of CHR engines, as recently happened with the Leuven CHR implementation [17]. Finally, those ALP which do not exploit abduction (or use abduction only in a limited subset of the application) do not suffer from the meta-interpretation overhead, but run at full speed. 2 However, a rule with a defined predicate in the antecedent is not allowed: these languages sacrifice negation by default on the altar of efficiency, which is a sensible thing to do in some applications, but it is not in others. The SCIFF proof-procedure [18] was developed in 2003 with an alternative CHR implementation, in which integrity constraints are first-class objects, and the proof-procedure can actively reason about them. In particular, we map ab- ducibles into CHR constraints and implement the transitions of the operational semanticsasCHR rules;inthisway,theimplementationfollowsverycloselythe operational semantics. Thanks to the sound operational semantics, SCIFF has a sound treatment of default (and also explicit) negation. Thanks to the CHR implementation, SCIFF is smoothly integrated with a constraint solver. From a language viewpoint, SCIFF has unique features that do not appear in other ab- ductive proof-procedures: it handles universally quantified variables both in the abducibles and in the integrity constraints; CLP constraints (treated as quan- tifier restrictions [19]) can be imposed both on existentially and on universally quantified variables. SCIFFhasbeencontinuouslydevelopedandimprovedinthepastfewyears, and now it is smoothly integrated in graphical interfaces, semantic web applica- tions; it is considerably faster, more robust, and provides more features. In this paper, we show the implementation in CHR of the abductive proof- procedure SCIFF, and we report about its recent improvements. The rest of the paper is organised as follows. We first describe the SCIFF abductiveframeworkinSection2.AftersomepreliminariesonCHR (Section3), we present the implementation of SCIFF in CHR (Section 4). Discussion of related work (Section 5) and conclusions (Section 6) follow. 2 An abductive framework Abductive Logic Programming is a family of programming languages that inte- grate 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 finding a set of abducibles ∆ ⊆ A that, together with the knowledge base, is an explanation for a given known effect (also called goal G): KB∪∆|=G. Also, ∆ should satisfy a set of logic formulae, called Integrity Constraints IC: KB∪∆|=IC. E.g., if a patient has a headache, a physician may consult a knowledge base headache←flu. headache←migraine. headache←meningitis. 3 and the abductive system will return one of the three explanations. SCIFF [18] is a language in the ALP class. CLP [20] constraints can be imposed on variables (which allows, for instance, to express that an event is expected to happen in a given time interval). For example, we might have an integrity constraint flu→temp(T),T <39 saying that the explanation flu is acceptable only if the temperature of the pa- tientislessthan39oC.Thecomputedanswerincludesingeneralthreeelements: 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 verification of interaction in multia- gent systems [21,22] and it is an extension of the IFF proof-procedure [7]. 3 A brief introduction to Constraint Handling Rules Constraint Handling Rules [12] (CHR for brevity hereafter) are essentially a committed-choice language consisting of guarded rules that rewrite constraints inastoreintosimpleronesuntiltheyaresolved.CHR definebothsimplification (replacing constraints by simpler constraints while preserving logical equiva- lence) and propagation (adding new, logically redundant but computationally useful, constraints) over user-defined constraints. 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: simplification, propagation and simpagation. Simplification CHRs. Simplification rules are of the form H ,...,H ⇐⇒G ,...,G |B ,...,B (1) 1 i 1 j 1 k with i > 0, j ≥ 0, k ≥ 0 and where the multi-head H ,...,H is a nonempty 1 i sequenceofCHR constraints,theguardG ,...,G isasequenceofbuilt-incon- 1 j straints,andthebodyB ,...,B isasequenceofbuilt-inandCHR constraints. 1 k Declaratively, a simplification rule states that, if the guard is true, then the left-hand-side and the right-hand-side are equivalent. Operationally, when constraint instances H ,...,H in the head are in the 1 i storeandtheguardG ,...,G istrue,theyarereplacedbyconstraintsB ,...,B 1 j 1 k in the body. Propagation CHRs. Propagation rules have the form H ,...,H =⇒G ,...,G |B ,...,B (2) 1 i 1 j 1 k where the symbols have the same meaning of those in the simplification rules (1). Declaratively, a propagation rule is an implication, provided that the guard istrue.Operationally,whentheconstraintsintheheadareinthestore,andthe guard is true, the constraints in the body are added to the store. 4 Simpagation CHRs. Simpagation rules have the form H ,...,H \H ,...,H ⇐⇒G ,...,G |B ,...,B (3) 1 l l+1 i 1 j 1 k where l > 0 and the other symbols have the same meaning and constraints of those of simplification CHRs (1). Declaratively, the rule of Eq. (3) is equivalent to H ,...,H ,H ,...,H ⇐⇒G ,...,G |B ,...,B ,H ,...,H (4) 1 l l+1 i 1 j 1 k 1 l Operationally,whentheconstraintsintheheadareinthestoreandtheguardis true,H ,...,H remaininthestore,andH ,...,H arereplacedbyB ,...,B . 1 l l+1 i 1 k Forexample,theconstraint≤canbeimplementedinCHRbygivingitsbase properties, namely the following rules: A≤A⇔true (5) A≤B,B ≤A⇔A=B (6) A≤B,B ≤C ⇒A≤C (7) where the symbol ’=’ stands for unification. The CHR engine rewrites the con- straints 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 unified, as prescribed by rule 6. Note that on the left-hand-side of a CHR rule only constraints defined with CHR can appear: while the right-hand-side can contain any Prolog predicate (including CLP(FD) constraints, unifications, etc.), these elements cannot appear on the left-hand-side. 4 Implementation of the SCIFF proof-procedure One of the features obtained through a CHR implementation (avoiding meta- interpretation) is that the resolvent of the proof is directly represented as the Prolog resolvent. This allows us to exploit the Prolog stack for depth-first ex- plorationofthetreeofstates.Moreimportantly,thismeansthatweextensively reuse the Prolog machinery, and that built-in predicates in the host Prolog sys- tem 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 proof- procedure3 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) li- braries, available both on SICStus [23] and SWI Prolog [24] We also have a 3 This constraint store, which contains CLP constraints over variables, should not be confusedwiththeCHRconstraintstore,whichisusedfortheimplementationofthe other data structures. 5 CHR-basedsolveronfiniteandinfinitedomains,andwedefinedanad-hoc solver forreifiedunification.Recently,theinterfacebetweenSCIFFandtheconstraint solverhasbeenre-engineered,andnowitallowsthedevelopertoadoptanycon- straintsolverthatimplementsagiveninterface.Inthisway,theusercanchoose for each application which solver he/she wants to use; moreover, new solvers can be added with very limited effort. For example, the constraint solver on the reals, CLP(R) [25] has been integrated into SCIFF: the new solver is based on thesimplexalgorithm(plusbranch-and-bound),whichisveryefficientforlinear constraints. To the best of our knowledge, the other abductive proof-procedures imple- mented in CHR map abducibles to CHR constraints. Integrity constraints, in- stead, are often represented as CHR rules (typically, propagation rules) [13,15]. Since a propagation CHR can have only CHR constraints in the multiple heads, thecorrespondingabductiveproof-procedurecancontainonlyabduciblesinthe precondition. This limitation forbids in the proof-procedure the implementation of default negation, that was one of the main motivations behind Abductive Logic Programming [9]. The operational semantics is then an extension of the operational semantics of CHR. SCIFFwasdevelopedfollowingadifferentidea:wewantedincreasedflexibil- ityinourlanguage,whileretainingthefeaturesthatcomeforfreewiththeCHR implementation. We first defined the declarative and operational semantics of SCIFF as extensions of the IFF [7]. The operational semantics is given through a set of transitions that transform a state into another. The implementation, whichmapsintegrityconstraints,aswellastheotherrelevantdatastrutures,to CHR constraints (rather than CHR rules) and transitions to CHR rules, follows the operational semantics very closely. In the following, we first show some examples of transitions; the interested reader can find the complete list of transitions in a previous publication [18], together with the proofs of soundness and completeness of the SCIFF proof- procedure. We then describe the implementation of some transitions in Sec- tion 4.2. 4.1 Examples of transitions Given an abducible a(X) and an integrity constraint a(Y)∧p(Z)∧Y >Z →r(Z) transitionpropagationgeneratesthefollowingimplication(thatwecallPartially 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 first we consider the case X =Y, so the previous implication is transformed into p(Z)∧X >Z →r(Z), 6 in the second node, we consider the case that X (cid:54)= Y, and in this case the implication (8) is already satisfied. Suppose we choose the first node, and that the knowledge base contains the definition 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 first node we consider the case X > 1, while in the second X ≤ 1. In the first case, the goal r(1) is invoked. These are just some examples of the transitions. SCIFF contains transi- tions for handling correctly the various items (abducibles, expectations, hap- pened 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 opera- tional 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 knowledgebase,andCHRwilltakecareofallthemachinerynecessarytoabduce a new literal and propagate its consequences. For example, the clause g(X):−a(X),b. can be written as g(X) :- abd(a(X)), b. A (partially solved) integrity constraint 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 first 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)), (9) reif_unify(X,Y1,B), (B#=1, psic(Rest1,Head1) ; B#=0). where copy performs a renaming of an atom (which also considers the various types of quantification in the SCIFF [18], as well as CLP constraints attached 7 to the variables), #= is the finite domain equality constraint and reif_unify is a CHR implementation of reified unification [26]. reif_unifyisaCHRconstraintthatdeclarativelyimposesthateitherB=1 and the first two arguments unify, or B=0 and the two atoms do not unify; in logics, reif_unify(X,Y,B) is true iff 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 whichPSICshavebeentriedwithwhichabducibles(inordertoavoidloops),as CHR itself does this work. Note also that propagation is attempted only with the first 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 efficientindexingandhashtablestoavoidcheckingallthepossiblepairsofCHR constraints.Sadly,rule(9)doesnotexploitsuchfeaturesofCHR.Notethatthe constraintsintheantecedentofthepropagationCHR donotshareanyvariable, 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 first idea would be to rewrite the transition as: abd(X), psic([abd(X)|Rest],Head) ==> ... whichwoulduseCHRhashtablesmuchmoreefficiently,butitwouldpropagate 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 reified unification algorithm. However, since abducibles are atoms, they always have a main functor, thus theargumentofabdisalwaysaterm,whichcancontainvariables,butitcannot 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 first 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). 8 Now,thepropagation transitioncanbeimplementedwiththeCHR propagation rule: abd(F,X), psic([abd(F,Y)|Rest],Head) ==> fn_ok(X,Y) | (10) copy(psic([abd(Y)|Rest],Head),psic([abd(Y1)|Rest1],Head1)), reif_unify(X,Y1,B), (B#=1, psic(Rest1,Head1) ; B#=0). i.e.,onlythosepairswithidenticalfirstargument(i.e.,abduciblesthatsharethe 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 efficiency. 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 thenon-deterministictransitions(thoseopeningchoicepoints),whileexpediting 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 defined 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.,wecheckifreifiedunificationimposedavalueonthebooleanvariableB,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 defined a set of CHRs for dealing with nondeterministic con- straints.Wealternateadeterministicandanon-deterministicphase:initially,in the derivation, only deterministic transitions can be activated. Later, when the fixedpointofthedeterministiconesisreached,onenon-deterministictransition can be applied, and we return to the deterministic phase. In CHR: switch2det @ phase(nondeterministic), nondeterministic(G) <=> call(G), 9 phase(deterministic). switch2nondet @ phase(deterministic) <=> phase(nondeterministic). where rule switch2nondet should be one of the last rules to be tried. TransitionUnfolding. DifferentlyfromHYPROLOG[15],integrityconstraints caninvolveliteralsbuiltondefinedpredicates.Thisallowsforasoundtreatment of default negation: a negative literal not(a) is converted into an implication a → false. Given a PSIC whose body contains a literal of a predicate defined in the KB, transition unfolding unfolds the literal: psic([Atom|Rest],Head) <=> is_defined_literal(Atom) | findall(clause(Atom,Body),clause(Atom,Body),Clauses), unfold(Clauses,psic([Atom|Rest],Head)). unfold([],_). unfold([clause(Atom,Body)|Clauses],psic([Atom1|Rest1],Head1)):- ccopy(psic([Atom1,Rest1],Head1),psic([Atom2|Rest2],Head2)), Atom = Atom2, append(Body,Rest2,NewBody), psic(NewBody,Head2), unfold(Clauses,psic([Atom1|Rest1],Head1)). This might pose problems of termination: if the unfolded predicate is recur- sive, there exists an infinite branch in the derivation. For example, consider the IC: a(List),member(Term,List)→b(Term) (11) with the knowledge base: member(X,[X|T]). member(X,[Y|T]):−member(X,T). g :−a([1,2,3]). Intuitively,thegoalg istrueprovidedthatweabducea([1,2,3])andb(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 infinite number of implica- tions. For this reason, early versions of SCIFF delay the unfolding after the othertransitions,inthehopeofbindingsomeofthevariables.Inthisparticular 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 finite. However,inothercasesdefinedpredicatesprovidejustthevalueofaparam- eter, in this example, a deadline: start(a,T )∧deadline(D)→end(b,T )∧T ≤T +D a b b a 10