Abductive Logic Programming is a computationally founded representation of abductive reasoning. In most ALP frameworks, integrity constraints express domain-speci c logical relationships that abductive answers are required to satisfy. Integrity constraints are usually known a priori. However, in some applications (such as interactive abductive logic programming, multi-agent interactions, contracting) it makes sense to relax this assumption, in order to let the abductive reasoning start with incomplete knowledge of integrity constraints, and to continue without restarting when new integrity 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, soundness and completeness properties) and an implementation of such a framework based on the SCIFF language and proof procedure.
The philosopher Charles Sanders Peirce divides the reasoning schemes of humans into three types: deduction (reasoning from causes to e ects), induction (synthesizing new rules from examples) and abduction (making hypotheses on possible causes from known e ects).
Abductive Logic Programming [
Several instances of ALP have been proposed in the literature [2{6], which di er 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 eld of abductive reasoning is the diagnosis. 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 re nes 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 exchange 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 rst tries to get a price as low as possible, while the second has the opposite aim, and they negotiate 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 rst 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
automated computational process; for instance, by inductive reasoning. Recently,
extensions of Inductive Logic Programming techniques (ILP for short), and the
DPML algorithm in particular [
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 [
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, soundness and completeness. In section 3 we discuss some possible applications. Discussion of related work and conclusions follow. 2
Runtime addition of integrity constraints in S CIFF In this section, we give a semantics for the runtime addition of integrity constraints for the SCIFF abductive logic language; however, the de nitions 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 de nition of the language is available in [
A SCIFF program P is composed of { a knowledge base KB; { a set ICS of static integrity constraints.
Predicates In SCIFF, predicates can be de ned or abducibles, and can contain
variables. Variables can be constrained as in Constraint Logic Programming [
Integrity constraints In SCIFF, integrity constraints have the form
where Body is a conjunction of abducible atoms, de ned atoms and constraints, and Head is a disjunction of conjunctions of abducible atoms and CLP constraints, 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
KakasMancarella [
Goal In SCIFF, a Goal has the same syntax of the body of a clause in the knowledge base. 2.2
A declarative semantics for runtime addition of integrity constraints can be given as follows.
Given a program P = hKB; ICS 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 ICD i
1. KB [
2. KB [
j= G
j= ICS [ ICD
where the symbol j= is interpreted, in SCIFF, as the 3-valued completion
semantics [
(1) (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): fa(2); b(2); d(2)g and fa(2); c(2); d(2)g.
However, with the additional integrity constraint only fa(2); b(2); d(2)g is an abductive answer.
p(X) q(X; Y ) r(2) q(X; Y ); a(Y ) r(Y ); d(Y ) a(X) ! b(X) _ c(X) c(X); d(X) ! false; 2.3
The SCIFF proof-procedure is a rewriting system that de nes 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 [
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
constraints, and is the current set of abduced literals. The main transitions,
inherited from the IFF are:
Unfolding replaces a (non abducible) atom with its de nitions;
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 simpli cations other simpli cations like (true ! A) , A, etc.
SCIFF includes also the transitions of CLP [
We extend SCIFF with an additional transition de ned 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 [ ficg; 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; ICS i, with additional integrity constraints ICD and a goal G is a sequence of nodes where { the root node is hG; ;; ICS ; ;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 quanti ed by a ground term; { satis es all the constraints in the store CS and the implications in P SIC.
If such a derivation exists, we write hKB; ICS i`hICD; iG. 2.4
SCIFFD properties can be derived from SCIFF properties, by showing that a SCIFFD derivation (successful or not) for the program hKB; ICS i with a nite set of additional integrity constraints ICD can be transformed in an equivalent one, where a node is the root node of a SCIFF derivation for the ALP hKB; ICS [ ICDi.
Due to how the addIC transition operates, the number of addIC transitions in a derivation is nite, if the set of additional integrity constraints is nite, because each addIC transition removes one integrity constraint from the queue, and the transition is not applicable when the queue is empty.
N1 T!1 N2 add!IC N3 N1 add!IC N4 T!1 N5 Proof. Let N1 hR1; CS1; P SIC1; 1i.
N2 hR2; CS2; P SIC2; 2i N3 hR2; CS2; P SIC2 [ ficg; 2i N4 hR1; CS1; P SIC1 [ ficg; 1i
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 [ ficg; 2i
addIC transition. Then there exists a derivation D0 that has the following properties: { the rst k transitions of D0 are the same applications of addIC; { each node of D0, starting the transitions from k + 1 is equal to the corresponding 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 [
Intuitively, for SLD resolution a level mapping must be de ned, 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
[
Termination is not a ected in SCIFFD, as long as the newly added integrity constraints do not violate the termination conditions.
Proof. Consider a SCIFFD derivation D, with root node hG; ;; ICS ; ;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; ;; ICS [ ICD; ;i. With the given hypotheses, such node is the initial node of a SCIFF derivation that is nite, 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 nite.
Soundness Since SCIFFD only di ers from SCIFF for the presence of addIC transitions, and addIC is only applicable for a non-empty set of additional integrity 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 [
We now extend it to the case with a (non-empty) set of additional integrity constraints ICD:
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; ;; ICS [ ICD; ;i. The rest of the D0 transition is a SCIFF derivation.
By the SCIFF soundness result (proposition 5),
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 [
such that
The corresponding result for SCIFFD, with non-empty set ICD is as follows. that hKB; ICS i`hICD0; iG and 0
.
straints, for any ground set such that hKB; ICS i ICD G there exists ' such Proof. By the SCIFF completeness result (proposition 7), there exists a SCIFF derivation whose root node is N = hG; ;; ICS [ ICD; ;i, and whose abductive answer is h ; i.
But N is a node in a successful SCIFFD derivation, whose root node is hG; ;; ICS ; ;i, and addIC is applied for all ICs in ICD. 2.5
The SCIFF abductive proof procedure was implemented in Prolog, using
extensively the Constraint Handling Rules [
Constraint Handling Rules (CHR) is a logic language devoted to de ne new constraint solvers; however, it has been used as a general language for many di erent applications, not all strictly related to constraints.
A new solver is de ned in CHR by means of rules. There exist two main types of rules: propagation and simpli cation3. A propagation rule is of the form
Head1; : : : ; Headn ) GuardjBody 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 identi er of the rule. 3 There are also simpagation rules, that are not logically necessary, but are important for e ciency; we will not go into details for lack of space. Simpli cation rules have a similar syntax:
Head1; : : : ; Headn , GuardjBody 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 represented as the CHR constraint
B{ozdy psic( [abd(a(Y)),q(Y)]; ( p(Y) ; abd(c(Y)) ) ) | } | }
H{ezad
The Head can be any Prolog goal (it has the same syntax).
The proof tree is explored in a depth- rst 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 simpli cation (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 constraints 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 red, it generates psic([a(X)=a(1)],b(X)), that triggers case analysis, which in its turn generates two children nodes: { one where uni cation is imposed between the abducible in the CHR constraint 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 disuni cation 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 rst case as X = 1 and b(X) is executed; in the second case by imposing the CLP constraint X 6= 1.
The relevant point, here, is that rule propagation is red whenever both the constraints (the abducible and the psic) are in the CHR store, regardless of which one entered the store rst. 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
Traditionally, diagnosis has been one of the most natural applications of abductive 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 nding any explanation, but the doctor can ask questions, and re ne 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 information 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 following relevant clauses in the knowledge base, where u, ulcera, some drug, and some food are abducibles: stomach ache u stomach ache ulcera spots some drug spots some food
The query posed by the doctor is stomach ache; spots. The abductive answers, equally plausible at this stage, are f u; some drugg, f u; some food g, fulcera; some drugg, and fulcera; some food g. To further investigate, the doctor asks the patient if he ate some food, or he is being treated with some drug. The 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 f u; some drug ; ulcerag, and fulcera; some drug g. The doctor may prefer the latter, for minimality. 3.2
In [
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 abductive 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 bene t is
twofold: rst, 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 identi ed. In Protune [
Many problems in constraint programming require a very large set of constraints, that cannot be propagated e ciently all at once. For example, integer linear programming relies on a linear solver, that solves very e ciently linear constraints (in some cases, with polynomial algorithms), but cannot handle natively the integrality 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 exponential. 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
webfriendly format (like RuleML or the RIF). SCIFF is currently able to download
web content through the PiLLoW library [
To show the e ectiveness of the approach, we tested a simple benchmark problem, that is a simpli ed 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 nd 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 nd the right service. As a comparison, a solution that rst downloads the IC of all possible services before starting the solution takes 319.005s.
Related work
Among the many works on abduction in CHR by Christiansen and colleagues [
EVOLP [
We can also easily extend the language in order to incorporate dynamic
integrity 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
[
In CR-Prolog [
Conclusions In this paper we proposed a declarative semantics for abductive logic programs where additional integrity constraints can be added at runtime. Such an extension 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.