Runtime Addition of Integrity Constraints in SCIFF? Marco Alberti1 , Marco Gavanelli2 , and Evelina Lamma2 1 CENTRIA, DI-FCT, Universidade Nova de Lisboa Quinta da Torre - 2825-144 Caparica (Portugal) m.alberti@fct.unl.pt 2 ENDIF, Università di Ferrara Via Saragat, 1 - 44100 Ferrara (Italy) marco.gavanelli@unife.it evelina.lamma@unife.it Abstract. Abductive Logic Programming is a computationally founded representation of abductive reasoning. In most ALP frameworks, in- tegrity constraints express domain-specific logical relationships that ab- ductive answers are required to satisfy. Integrity constraints are usually known a priori. However, in some ap- plications (such as interactive abductive logic programming, multi-agent interactions, contracting) it makes sense to relax this assumption, in or- der to let the abductive reasoning start with incomplete knowledge of integrity constraints, and to continue without restarting when new in- tegrity constraints become known. In this paper, we propose a declarative semantics for abductive logic programming with addition of integrity constraints during the abductive reasoning process. We propose an operational instantiation (with formal termination, sound- ness and completeness properties) and an implementation of such a framework based on the SCIFF language and proof procedure. 1 Introduction The philosopher Charles Sanders Peirce divides the reasoning schemes of hu- mans into three types: deduction (reasoning from causes to effects), induction (synthesizing new rules from examples) and abduction (making hypotheses on possible causes from known effects). Abductive Logic Programming [1] is a computational representation of ab- ductive reasoning that allows to express relationships between effects and possi- ble causes (by means of a logic program), as well as logical constraints over the hypotheses (integrity constraints). In ALP possible hypotheses are represented by special predicates (called abducibles) that are not defined, but can be hy- pothesized, as long as they satisfy the integrity constraints. A positive answer to a query posed to an ALP system will typically contain the set of abducibles ? A short version of this paper will appear as LIPIcs technical communication. that are hypothesized in order for the query to succeed. Such an answer is called abductive answer in the ALP literature. Several instances of ALP have been proposed in the literature [2–6], which differ for the logic language (and in particular for the type of abducibles and of integrity constraints that can be expressed). While in many applications integrity constraints are known at the beginning of the reasoning process, it is sometimes useful to relax this assumption. For instance, the classical application field of abductive reasoning is the di- agnosis. However, in a realistic setting, a doctor does not simply listen to the patient enumerating all his/her symptoms. Instead, they have a bidirectional and multi-stage interaction: the doctor asks questions and refines his/her diagnosis based on the answers of the patient. So, there is the need to add information dynamically, often in the form of rules, that can rule out unrealistic sets of explanations. In multi-agent reasoning, agents that employ abductive reasoning could ex- change integrity constraints by a communication process, and continue operating with the newly acquired integrity constraints. In contracting, two agents try to reach an agreement and each agent tries to reach its goals. For example, one agent may want to buy a car, and the other wants to sell it; the first tries to get a price as low as possible, while the second has the opposite aim, and they nego- tiate on the model, the optionals, etc. Of course, each agent is unwilling to send all of its own knowledge, because the other would exploit it to get favourable conditions: if the buyer knew all the constraints of the seller, it would be able to compute the minimum possible price for the seller, and then propose such price. On the other hand, it is quite natural to tell some of the constraints only when needed, in order to speedup the negotiation, and avoid lingering on small variations of a meaningless solution. For instance, in case the buyer asks for a seat for children, the seller could reply: “Ok, but you cannot install a children seat if you have the airbag”, and the client has to take into consideration this constraint, when making new proposals. On the other hand, there is no reason for the seller to state such knowledge immediately from the beginning, as it still does not know if the buyer is interested at all in children seats. An abductive reasoner might seek additional integrity constraints (possibly available from public repositories), depending on its current computation; for example, the number of integrity constraints could be very vast (as if one has to take into consideration all the EU rules for contracts), so only those strictly needed should be downloaded. Moreover, depending on the current state of the derivation one may choose to download regulations from one server or another: suppose I am deciding whether to buy a good from a service in Italy or in Portugal; I may first try to get the best price, but then check if the regulations of that country allow me to do such transaction. I will download the regulations of such country, check if my transaction is allowed, and, if it is not, I will backtrack and take the second choice. Integrity constraints can also be obtained at runtime by means of an au- tomated computational process; for instance, by inductive reasoning. Recently, 2 extensions of Inductive Logic Programming techniques (ILP for short), and the DPML algorithm in particular [7], have been proposed to learn integrity con- straints from labelled traces (a database of events recording happened inter- actions or activities, or a database collecting events at run-time). The DPML target language is the SCIFF abductive logic language [8], and this inductive approach has been experimented in various contexts (business processes, among others; see [9, 10]). Such applications motivate an abductive logic programming framework where some of the integrity constraints are known in advance, and some are added to the abductive logic program during the computation. In this paper we propose such an extension, and a declarative semantics for it. We describe the instantiation and implementation of the extension in the SCIFF abductive logic language [8]. SCIFF is implemented using Constraint Handling Rules [11]; in particular, integrity constraints are mapped to CHR constraints. Thanks to the properties of CHR, adding a new constraint at run- time amounts to the single operation of calling the new constraint, i.e., it can be delegated to the CHR solver. The paper is structured as follows. In section 2, we propose a declarative semantics of ALPs with dynamic addition of integrity constraints based on the SCIFF language, and we show that it exhibits properties of termination, sound- ness and completeness. In section 3 we discuss some possible applications. Dis- cussion of related work and conclusions follow. 2 Runtime addition of integrity constraints in SCIFF In this section, we give a semantics for the runtime addition of integrity con- straints for the SCIFF abductive logic language; however, the definitions can be easily generalized for other abductive logic languages. 2.1 SCIFF language In the following, we provide a brief introduction to the SCIFF language, and, in particular, on how the knowledge base, integrity constraints and goals are expressed. A complete definition of the language is available in [8]. A SCIFF program P is composed of – a knowledge base KB; – a set IC S of static integrity constraints. Predicates In SCIFF, predicates can be defined or abducibles, and can contain variables. Variables can be constrained as in Constraint Logic Programming [12]. Knowledge base In SCIFF, the knowledge base is a set of clauses of the form Head ← Body where Head is an atom built on a defined predicate, and body is a conjunction of literals (built on defined predicates or abducibles) and CLP constraints. 3 Integrity constraints In SCIFF, integrity constraints have the form Body → Head where Body is a conjunction of abducible atoms, defined atoms and constraints, and Head is a disjunction of conjunctions of abducible atoms and CLP con- straints, or false. The allowed integrity constraints vary in ALP languages. For instance, they can state that a given conjunction of literals implies false (as in the Kakas- Mancarella [2] language); or that a conjunction of atoms implies a disjunction of atoms (as in the IFF language [3]). Goal In SCIFF, a Goal has the same syntax of the body of a clause in the knowledge base. 2.2 Declarative semantics A declarative semantics for runtime addition of integrity constraints can be given as follows. Given a program P = hKB, IC S i and a goal G, a pair h∆, θi, where ∆ is a set of abducibles and θ is a substitution, is an abductive explanation for G with additional integrity constraints IC D iff 1. KB ∪ ∆ |= Gθ 2. KB ∪ ∆ |= IC S ∪ IC D where the symbol |= is interpreted, in SCIFF, as the 3-valued completion se- mantics [13]. If such conditions hold, we write hKB, IC S i∆ IC D G. Example 1. p(X) ← q(X, Y ), a(Y ) q(X, Y ) ← r(Y ), d(Y ) (1) r(2) a(X) → b(X) ∨ c(X) (2) Given the knowledge base in equation (1) and the integrity constraint in equation (2), where a/1, b/1, c/1, and d/1 are abducibles, two abductive answers are possible for the query p(1): {a(2), b(2), d(2)} and {a(2), c(2), d(2)}. However, with the additional integrity constraint c(X), d(X) → false, only {a(2), b(2), d(2)} is an abductive answer. 4 2.3 Operational semantics The SCIFF proof-procedure is a rewriting system that defines a proof tree, whose nodes represents states of the computation. A set of transitions that rewrite a node into one or more children nodes. SCIFF inherits the transitions of the IFF proof-procedure [3], and extends it in various directions. We recall the basics of SCIFF; a complete description is in [8], with proofs of soundness, completeness, and termination. Each node of the proof is a tuple T ≡ hR, CS, P SIC, ∆i, where R is the resolvent, CS is the CLP constraint store, PSIC is a set of implications (called Partially Solved Integrity Constraints) derived from propagation of integrity con- straints, and ∆ is the current set of abduced literals. The main transitions, inherited from the IFF are: Unfolding replaces a (non abducible) atom with its definitions; Propagation if an abduced atom a(X) occurs in the condition of an IC (e.g., a(Y ) → p), the atom is removed from the condition (generating X = Y → p); Case Analysis given an implication containing an equality in the condition (e.g., X = Y → p), generates two children in logical or (in the example, either X = Y and p, or X 6= Y ); Equality rewriting rewrites equalities as in the Clark’s equality theory; Logical simplifications other simplifications like (true → A) ⇔ A, etc. SCIFF includes also the transitions of CLP [12, 14] for constraint solving. We extend SCIFF with an additional transition defined as follows, and we call the resulting proof procedure SCIFFD . Add IC Given a node T ≡ hR, CS, P SIC, ∆i and an integrity constraint ic, transition addIC generates one node T 0 ≡ hR, CS, P SIC ∪ {ic}, ∆i. This transition picks integrity constraints from a queue of dynamic integrity constraints. The transition is applicable to any node in the proof tree, and it can be executed whenever the queue is not empty. More integrity constraints can be added to the queue during the computation. Successful derivation A successful SCIFFD derivation for an ALP hKB, IC S i, with additional integrity constraints IC D and a goal G is a sequence of nodes where – the root node is hG, ∅, IC S , ∅i – each node is generated from the previous one by a SCIFFD transition – the leaf node is N ≡ htrue, CS, P SIC, ∆i From the leaf node, a substitution θ is derived, that – replaces all variables in N that are not universally quantified by a ground term; – satisfies all the constraints in the store CS and the implications in P SIC. h∆,θi If such a derivation exists, we write hKB, IC S i`IC D G. 5 2.4 Properties SCIFFD properties can be derived from SCIFF properties, by showing that a SCIFFD derivation (successful or not) for the program hKB, IC S i with a finite set of additional integrity constraints IC D can be transformed in an equiva- lent one, where a node is the root node of a SCIFF derivation for the ALP hKB, IC S ∪ IC D i. Due to how the addIC transition operates, the number of addIC transitions in a derivation is finite, if the set of additional integrity constraints is finite, because each addIC transition removes one integrity constraint from the queue, and the transition is not applicable when the queue is empty. Proposition 1. Let N2 be the node generated from node N1 by transition T1 , and N3 be the node generated from node N2 by addIC. Then, if N4 is the node generated from node N1 by addIC, transition T1 is applicable to N4 , and the node N5 generated from N4 by T1 is equal to N3 , modulo renaming of variables. 1T addIC N1 −→ N2 −→ N3 addIC 1 T N1 −→ N4 −→ N5 Proof. Let N1 ≡ hR1 , CS1 , P SIC1 , ∆1 i. From the statement of the proposition, we can write the other nodes as: N2 ≡ hR2 , CS2 , P SIC2 , ∆2 i N3 ≡ hR2 , CS2 , P SIC2 ∪ {ic}, ∆2 i N4 ≡ hR1 , CS1 , P SIC1 ∪ {ic}, ∆1 i Since N4 only differs from N1 for the presence of an additional IC, T1 is applicable on N4 , and it produces the same elements in the resulting node N5 , with an additional integrity constraint. That is, modulo renamings of variables, N5 ≡ hR2 , CS2 , P SIC2 ∪ {ic}, ∆2 i Proposition 2. Let D be a SCIFFD derivation that has k applications of the addIC transition. Then there exists a derivation D0 that has the following prop- erties: – the first k transitions of D0 are the same applications of addIC; – each node of D0 , starting the transitions from k + 1 is equal to the corre- sponding node of D. Proof. Trivially, by proposition 1, D0 is obtained from D by moving the addIC transition to the beginning. Termination Being SCIFF based on the 3-valued completion semantics, its termination is proven, as for SLDNF resolution [15], for acyclic knowledge bases and bounded goals and implications. Of course, programs may also terminate in other cases as well. Other abductive proof-procedures are based on other semantics and can address also non-stratified programs [16]. 6 Intuitively, for SLD resolution a level mapping must be defined, such that the head of each clause has a higher level than the body. For SCIFF, as well as for the IFF, since it contains integrity constraints that are propagated forward, the level mapping should also map atoms in the body of an integrity constraint to higher levels than the atoms in the head; moreover, this should also hold considering possible unfoldings of literals in the body of an integrity constraint [17]. An atom is bounded w.r.t. a level mapping if the level mapping is bounded over the ground instances of that atom; an implication is bounded if all its literals are. The following proposition is the SCIFF termination result [8]. Proposition 3. Let G be a query to an ALP hKB, IC S i, where KB S , IC S and G are acyclic w.r.t. some level mapping, and G and all implications in IC S are bounded w.r.t. the level-mapping. Then, every SCIFF derivation for each instance of G is finite. Termination is not affected in SCIFFD , as long as the newly added integrity constraints do not violate the termination conditions. Proposition 4. Let G be a query to an ALP hKB, IC S i, with additional integrity constraints IC D , where KB S , IC S ∪ IC D and G are acyclic w.r.t. some level mapping, and G and all implications in IC S ∪ IC D are bounded w.r.t. the level- mapping. Then, every SCIFFD derivation for each instance of G is finite. Proof. Consider a SCIFFD derivation D, with root node hG, ∅, IC S , ∅i. Then consider a derivation D0 , equal to D, except that all the addIC transitions are applied at the beginning. The node resulting from the last addIC transition is hG, ∅, IC S ∪ IC D , ∅i. With the given hypotheses, such node is the initial node of a SCIFF derivation that is finite, by the SCIFF termination result (proposition 3). Since, by proposition 2, D is equal to D0 for the part that follows the last addIC transition, D is also finite. Soundness Since SCIFFD only differs from SCIFF for the presence of addIC transitions, and addIC is only applicable for a non-empty set of additional in- tegrity constraints, a SCIFFD derivation for an empty set of additional integrity constraints is a SCIFF derivation for the same ALP. Therefore, the SCIFF soundness result [8] can be expressed as follows. Proposition 5. Given an ALP hKB, IC S i, if h∆,θi hKB, IC S i`∅ G then hKB, IC S i∆ ∅ Gθ We now extend it to the case with a (non-empty) set of additional integrity constraints IC D : Proposition 6. Given an ALP hKB, IC S i, if h∆,θi hKB, IC S i`IC D G then hKB, IC S i∆ IC D Gθ 7 Proof. Let D be a successful SCIFFD derivation. By proposition 2, for the part after the last addIC transition, D is equal to a derivation D0 where all the addIC transitions are applied at the beginning. The node after the last addIC transition in D0 is hG, ∅, IC S ∪ IC D , ∅i. The rest of the D0 transition is a SCIFF derivation. By the SCIFF soundness result (proposition 5), hKB, IC S i∆IC D Gθ Completeness Due to the fact that, as explained earlier, a SCIFFD derivation for an empty set of additional integrity constraint is also a SCIFF derivation for the same ALP, the SCIFF completeness result [8] can be expressed as follows. Proposition 7. Given an ALP hKB, IC S i and, for any ground set ∆ such that h∆0 ,θi hKB, IC S i∆ ∅ G there exists ∆’ such that hKB, IC S i`∅ G, and ∆0 θ ⊆ ∆ The corresponding result for SCIFFD , with non-empty set IC D is as follows. Proposition 8. Given an ALP hKB, IC S i and a set IC D of integrity con- straints, for any ground set ∆ such that hKB, IC S i∆ IC D G there exists ∆’ such h∆0 ,θi that hKB, IC S i`IC D G and ∆0 θ ⊆ ∆. Proof. By the SCIFF completeness result (proposition 7), there exists a SCIFF derivation whose root node is N = hG, ∅, IC S ∪ IC D , ∅i, and whose abductive answer is h∆, θi. But N is a node in a successful SCIFFD derivation, whose root node is hG, ∅, IC S , ∅i, and addIC is applied for all ICs in IC D . 2.5 Implementation The SCIFF abductive proof procedure was implemented in Prolog, using exten- sively the Constraint Handling Rules [11, 18] library. The implementation can be downloaded from the SCIFF web site [19] and runs on SICStus and SWI Prolog. Constraint Handling Rules (CHR) is a logic language devoted to define new constraint solvers; however, it has been used as a general language for many different applications, not all strictly related to constraints. A new solver is defined in CHR by means of rules. There exist two main types of rules: propagation and simplification3 . A propagation rule is of the form label@ Head1 , . . . , Headn ⇒ Guard|Body and means that, if the optional Guard and the Heads are true, then the Body must be true. Operationally, whenever a set of constraints are in the store, matching Head1 , . . . , Headn , the Guard is checked; if it evaluates to true, the Body is executed (as a Prolog goal). The label is optional and serves only as an identifier of the rule. 3 There are also simpagation rules, that are not logically necessary, but are important for efficiency; we will not go into details for lack of space. 8 Simplification rules have a similar syntax: label@ Head1 , . . . , Headn ⇔ Guard|Body They state that if the Guard is true, then the conjunction Head1 , . . . , Headn is equivalent to Body. Operationally, if Head1 , . . . , Headn are in the store (and Guard is true), they are removed and substituted by Body. SCIFF represents most of its data structures as CHR constraints: – an abducible atom a(X) is represented with the CHR constraint abd(a(X)) – a (partially solved) integrity constraint a(Y ), q(Y ) → p(Y ) ∨ c(Y ) is repre- sented as the CHR constraint psic( [abd(a(Y)),q(Y)], ( p(Y) ; abd(c(Y)) ) ) | {z } | {z } Body Head The Head can be any Prolog goal (it has the same syntax). The proof tree is explored in a depth-first fashion, using the Prolog stack for this purpose. Transitions are implemented as CHR rules; for example, transition Propagation is implemented with the following propagation CHR: propagation @ abd(A1), psic([abd(A2)|More],Head) ==> psic([A1=A2|More],Head). Case Analysis handles the equality in the body of a PSIC case_analysis @ psic([A=B|More],Head) ==> impose A=B psic(More,Head) ; % Open choice point impose A and B do not unify and the logical simplification (true → A) ⇔ A manages implications with empty body: logic_simplification @ psic([],Head) <=> call(Head). Thanks to this implementation, adding a new integrity constraint is just a matter of calling the corresponding CHR constraint: if we want to dynamically add the integrity constraint (2) we execute the goal: psic( [abd(a(X))], (abd(b(X));abd(c(X))) ). In this way, the newly added integrity constraint is automatically subject to all the applicable transitions. Consider rule propagation: whenever two con- straints matching the rule head (e.g., abd(a(1)) and psic([a(X)],b(X))) are present in the CHR constraint store, the rule is fired, it generates psic([a(X)=a(1)],b(X)), that triggers case analysis, which in its turn generates two children nodes: 9 – one where unification is imposed between the abducible in the CHR con- straint store and the abducible in the partially solved integrity constraint, and a new partially solved integrity constraint is imposed, with the abducible removed from the body. – one where disunification between the abducible in the CHR constraint store and the abducible in the partially solved integrity constraint is imposed. In the previous example, psic([a(X)=a(1)],b(X)) is rewritten in the first case as X = 1 and b(X) is executed; in the second case by imposing the CLP con- straint X 6= 1. The relevant point, here, is that rule propagation is fired whenever both the constraints (the abducible and the psic) are in the CHR store, regardless of which one entered the store first. So, if a partially solved integrity constraint is added by addIC , and some abducible in its body is already in the store, propagation will occur, as if the partially solved integrity constraint had been in the constraint store from the beginning of the computation. 3 Applications In this section, we show some typical applications of abductive reasoning where runtime addition of integrity constraints can be of use. 3.1 A diagnosis scenario Traditionally, diagnosis has been one of the most natural applications of abduc- tive reasoning, as it amounts at making hypotheses about the possible causes of given symptoms. However, usually a diagnosis is not just a matter of listing all symptoms, and finding any explanation, but the doctor can ask questions, and refine his/her idea based on the received answers. In the same way, an expert system based on abductive reasoning should be able to receive more informa- tion dynamically, and continue its computation based on the new information available. Consider a patient that shows up at the doctor’s with stomach ache and spots on his face. The abduction-based diagnosis system used by the doctor has the follow- ing relevant clauses in the knowledge base, where flu, ulcera, some drug, and some food are abducibles: stomach ache ← flu stomach ache ← ulcera spots ← some drug spots ← some food The query posed by the doctor is stomach ache, spots. The abductive an- swers, equally plausible at this stage, are {flu, some drug}, {flu, some food }, {ulcera, some drug}, and {ulcera, some food }. To further investigate, the doctor asks the patient if he ate some food, or he is being treated with some drug. The 10 patient says that he does not eat some food, but he is taking some pills; however he knows that some drug gives him ulcera. The doctor now has two pieces of information that are relevant for this patient only: she adds dynamically the integrity constraints some food → false some drug → ulcera to the abductive logic program. The abductive answers are now {flu, some drug, ulcera}, and {ulcera, some drug}. The doctor may prefer the latter, for minimality. 3.2 Contracting in Service-Oriented Architectures In [20], we (with co-authors) proposed an automated contracting system for service-oriented architectures. In our architecture, a number of service providers expose their policies, expressed in the SCIFF language: in particular, integrity constraints represent pieces of policies in form of rules (for instance, if a cus- tomer wants to pay by bank transfer, the amount is expected to be credited by one week after the order), and domain-specific knowledge is expressed as SCIFF knowledge base clauses and, where appropriate, by ontologies (such as the con- cept of accepted customer). A user will also have policies expressed in the SCIFF language. In this application, abducibles represent actions by the users or the service providers (such as a message containing the credit card number, or the delivery of digital content). The heart of the system is the SCIFF Reasoning Engine (SRE). It receives as input a service provider’s and a user’s policies, as well as a user goal (such as the expectation to receive an ebook by one week). The system queries the SCIFF proof procedure with the goal, using the union of the policies as the ab- ductive program. The abductive answer, if one exists, is a sequence of abducibles that represent service provider’s and user’s actions, that achieve the goal while complying with the service provider’s and the user’s policies. Runtime addition of integrity constraints would allow starting the reasoning with a subset of the policies, and to incrementally add policies. The benefit is twofold: first, not to waste computational resources to search for solutions that are already ruled out by partial policies; second, the user or service providers may not want to disclose all of their policies unnecessarily, but only when potential contractors (based on partial policies) have been identified. In Protune [21], provisional predicates are ground atoms that can change their values as result of actions carried out by a peer (e.g., providing a credential). In our framework, it would be possible for agents to exchange (partial) policies expressed in the rich SCIFF language. 3.3 Abductive reasoning on the Web Many problems in constraint programming require a very large set of constraints, that cannot be propagated efficiently all at once. For example, integer linear pro- gramming relies on a linear solver, that solves very efficiently linear constraints 11 (in some cases, with polynomial algorithms), but cannot handle natively the in- tegrality constraints (i.e., the fact that some of the variables are required to have integer values). Integrality can be dealt with by adding more linear constraints (for example, Gomory cuts), but the number of such constraints can be expo- nential. The usually adopted solution is to add those constraints during search: if in the current candidate solution some variable X is not integer, only those constraints that remove the non-integral value of X are imposed. In the same way, the SCIFF proof-procedure can deal with problems with a very large number of integrity constraints. For example, laws or regulations can be expressed in the SCIFF language, and published on a web site, in some web- friendly format (like RuleML or the RIF). SCIFF is currently able to download web content through the PiLLoW library [22] and interpret data published in RuleML, so it can download from web servers a set of rules, interpret them as integrity constraints, and produce abductive answers that satisfy them. On the other hand, the set of regulations could be very wide, and downloading all of them could be a waste of time and bandwidth. Thanks to the dynamic addition of integrity constraints, SCIFF could download only those rules that involve the current set of abduced literals, impose them to rule out inconsistent explanations, and iteratively provide more and more refined solutions, in an interactive procedure. 3.4 Experiments To show the effectiveness of the approach, we tested a simple benchmark prob- lem, that is a simplified version of a contracting scenario of Section 3.2. One agent needs to interact with some web service, and choose one that is able to provide the expected reply. In this example, the agent will tell message m and will expect n as reply. The agent knows the address of a series of web services, given as facts: known service(http : //web.address.one/f older1/policy.ruleml). known service(http : //web.address.two/f older2/policy.ruleml). In order to find the right service, the agent executes the following goal, where tell is abducible: known service(Addr), download ic(Addr), tell(me, S, m), not(tell(S, me, A), A 6= n) meaning that it will non-deterministically choose a service, download its integrity constraints, and then tell message m; it will fail if it gets any reply that is not n. We generated 252 services, each with one integrity constraint tell(Client, s, letter1 ) → tell(s, Client, letter2 ) where letter1 and letter2 are substituted with a ground term corresponding to one of the 25 letters of the alphabet. We tried the goal on a slow network (mobile phone) and it took 173.350s to find the right service. As a comparison, a solution that first downloads the IC of all possible services before starting the solution takes 319.005s. 12 4 Related work Among the many works on abduction in CHR by Christiansen and colleagues [23, 24], we emphasize an inspiring position paper [25], in which preliminary experi- ments are shown with integrity constraints mapped to CHR rules. In that work, Christiansen points out that through meta-rules it is possible to dynamically add integrity constraints. Here we extend the idea within the SCIFF frame- work, which gives us a set of properties deemed crucial in the computational logic community. The operational semantics of SCIFF is not based on that of CHR, but on the sound and complete semantics of the IFF [3]: this allowed us to prove those properties also for SCIFF. In this paper, we extend these proofs for the dynamic addition of integrity constraints, reaching the objective pointed out by Christiansen, but with soundness and completeness results. EVOLP [26] is a language to define logic programs able to evolve. A special atom assert(Rule) can occur in the head or in the body of clauses; in case the stable model semantics assigns value true to some of these literals, the clause Rule is added to the program. Our instance can be considered as an evolving abductive program, in which only integrity constraints (and not clauses in the KB) can be added, and based on the three-valued completion semantics, instead of the stable model semantics. Our language also features CLP constraints and, as the general CLP framework [12], it is parametric with respect to the specific sort. The proof procedure lets the user choose the associated solver, and two state-of-the-art solvers are available in the current implementation: CLP(R), on the real values, and CLP(FD), on finite domains. EVOLP is a component of the ACORDA prospective logic programming system [16], which also integrates abductive reasoning and preferences, to support interactive abductive logic pro- gramming, among other applications. We can also easily extend the language in order to incorporate dynamic in- tegrity constraints in the body of clauses, or in queries. Operationally, whenever an integrity constraint is part of the resolvent, the addIC transition would be applied. However, the impact of such extension on termination must be studied in future work. With reference to nested, dynamic ICs, and this extension of the SCIFF language, it is worth to mention that in the literature, a lot of work was devoted to the treatment of embedded implications (due to Miller, et al. see [27, 28] and McCarty, see [29]) based on the logic of Higher-Order Hereditary Harrop Formulas, a fragment of Intuitionistic logic. In this logic, and the λ sys- tem implemented [30], they allow arbitrary lambda terms with full higher-order unification, and extend the formula language with arbitrarily nested universal quantifiers and implications. In our case, we can add integrity constraints at runtime, rather than program clauses as they do. We can therefore support ab- ductive reasoning in an extended set of constraints. In CR-Prolog [31], new (consistency-restoring) rules can be added dynam- ically, as a part of Observe-Think-Act loop of an agent; if some inconsistency is detected then these constraints can be considered, according to their prefer- ences. The semantics of CR-Prolog programs is defined as a transformation into abductive logic programs, where each consistency-restore rule has an abducible 13 associated with it, and holds (only) if such abducible is abduced. In our frame- work, dynamically added integrity constraints must be satisfied, independently of the abductive answer. 5 Conclusions In this paper we proposed a declarative semantics for abductive logic programs where additional integrity constraints can be added at runtime. Such an ex- tension can support interesting applications such as interactive abductive logic programming and contracting in service-oriented architecture. We proposed an operational instantiation of such a framework as the SCIFFD proof procedure, an extension of the SCIFF abductive proof procedure, and we proved formal results of termination, soundness, and completeness for SCIFFD . References 1. Kakas, A.C., Kowalski, R.A., Toni, F.: Abductive Logic Programming. Journal of Logic and Computation 2 (1993) 719–770 2. Kakas, A.C., Mancarella, P.: On the relation between Truth Maintenance and Abduction. In Fukumura, T., ed.: Proceedings of the 1st Pacific Rim International Conference on Artificial Intelligence, PRICAI-90, Nagoya, Japan, Ohmsha Ltd. (1990) 438–443 3. Fung, T.H., Kowalski, R.A.: The IFF proof procedure for abductive logic program- ming. Journal of Logic Programming 33 (1997) 151–165 4. Denecker, M., De Schreye, D.: SLDNFA: An abductive procedure for abductive logic programs. Journal of Logic Programming 34 (1998) 111–167 5. Alferes, J.J., Pereira, L.M., Swift, T.: Well-founded abduction via tabled dual programs. In De Schreye, D., ed.: ICLP. (1999) 426–440 6. Wang, K.: Argumentation-based abduction in disjunctive logic programming. Jour- nal of Logic Programming 45 (2000) 105–141 7. Lamma, E., Mello, P., Riguzzi, F., Storari, S.: Applying inductive logic program- ming to process mining. In Blockeel, H., Ramon, J., Shavlik, J.W., Tadepalli, P., eds.: ILP. Volume 4894 of Lecture Notes in Computer Science., Springer (2007) 132–146 8. Alberti, M., Chesani, F., Gavanelli, M., Lamma, E., Mello, P., Torroni, P.: Ver- ifiable agent interaction in abductive logic programming: the SCIFF framework. ACM Transactions on Computational Logics 9 (2008) 9. Chesani, F., Lamma, E., Mello, P., Montali, M., Riguzzi, F., Storari, S.: Exploiting inductive logic programming techniques for declarative process mining. T. Petri Nets and Other Models of Concurrency 2 (2009) 278–295 10. Lamma, E., Mello, P., Montali, M., Riguzzi, F., Storari, S.: Inducing declarative logic-based models from labeled traces. In Alonso, G., Dadam, P., Rosemann, M., eds.: BPM. Volume 4714 of Lecture Notes in Computer Science., Springer (2007) 344–359 11. Frühwirth, T.: Theory and practice of constraint handling rules. Journal of Logic Programming 37 (1998) 95–138 12. Jaffar, J., Maher, M.: Constraint logic programming: a survey. Journal of Logic Programming 19-20 (1994) 503–582 14 13. Kunen, K.: Negation in logic programming. Journal of Logic Programming 4 (1987) 289–308 14. Jaffar, J., Maher, M., Marriott, K., Stuckey, P.: The semantics of constraint logic programs. Journal of Logic Programming (1994) 15. Apt, K.R., Bezem, M.: Acyclic programs. New Generation Computing 9 (1991) 335–364 16. Lopes, G., Pereira, L.M.: Prospective programming with ACORDA. In: Empir- ically Successful Computerized Reasoning (ESCoR’06) workshop at The 3rd In- ternational Joint Conference on Automated Reasoning (IJCAR’06), Seattle, USA (2006) 17. Xanthakos, I.: Semantic Integration of Information by Abduction. PhD thesis, Im- perial College London (2003) Available at http://www.doc.ic.ac.uk/ ix98/PhD.zip. 18. Schrijvers, T., Demoen, B.: The K.U. Leuven CHR system: implementation and application. In Fruhwirth, T., Meister, M., eds.: First Workshop on Constraint Handling Rules. (2004) 19. Alberti, M., Chesani, F., Gavanelli, M.: The SCIFF abductive proof procedure (2004) http://lia.deis.unibo.it/research/sciff/. 20. Alberti, M., Cattafi, M., Gavanelli, M., Lamma, E., Chesani, F., Montali, M., Mello, P., Torroni, P.: Integrating abductive logic programming and description logics in a dynamic contracting architecture. In Hofmann, P., ed.: ICWS 2009: 2009 IEEE International Conference on Web Services, IEEE Computer Society, IEEE Computer Society Press (2009) 254–261 21. Coi, J.L.D., Olmedilla, D., Bonatti, P.A., Sauro, L.: Protune: A framework for semantic web policies. In Bizer, C., Joshi, A., eds.: International Semantic Web Conference (Posters & Demos). Volume 401 of CEUR Workshop Proceedings., CEUR-WS.org (2008) 22. Gras, D.C., Hermenegildo, M.V.: Distributed WWW programming using (Ciao-) Prolog and the PiLLoW library. TPLP 1 (2001) 251–282 23. Abdennadher, S., Christiansen, H.: An experimental CLP platform for integrity constraints and abduction. In Larsen, H.L., Kacprzyk, J., Zadrozny, S., Andreasen, T., Christiansen, H., eds.: FQAS, Heidelberg, Physica-Verlag (2000) 141–152 24. Christiansen, H., Dahl, V.: HYPROLOG: A new logic programming language with assumptions and abduction. In Gabbrielli, M., Gupta, G., eds.: ICLP. Volume 3668 of Lecture Notes in Computer Science., Springer (2005) 159–173 25. Christiansen, H.: Experiences and directions for abduction and induction using constraint handling rules. In: Workshop on abduction and induction AIAI’05, Edinburgh, Scotland (2005) 26. Alferes, J.J., Brogi, A., Leite, J.A., Pereira, L.M.: Evolving logic programs. In Flesca, S., Greco, S., Leone, N., Ianni, G., eds.: JELIA. Volume 2424 of Lecture Notes in Computer Science., Springer (2002) 50–61 27. Miller, D.: A logical analysis of modules in logic programming. Journal of Logic Programming 6 (1989) 79–108 28. Hodas, J.S., Miller, D.: Logic programming in a fragment of intuitionistic linear logic. Inf. Comput. 110 (1994) 327–365 29. McCarty, L.T.: Clausal intuitionistic logic I - fixed-point semantics. Journal of Logic Programming 5 (1988) 1–31 30. Nadathur, G., Miller, D.: An overview of lambda-prolog. In: ICLP/SLP. (1988) 810–827 31. Balduccini, M., Gelfond, M.: Logic programs with consistency-restoring rules. In: AAAI Spring 2003 Symposium. (2003) 9–18 15