Abduction with Hypotheses Confirmation

1 Introduction

Abductive Logic Programming (ALP) is an extension of Logic Programming to formalise hypothetical reasoning. It typically distinguishes between facts, defined within a static theory and known to be true or false, and potentially true, abducible atoms (hypotheses).

Abduction with Hypotheses Confirmation∗

Marco Alberti1 , Marco Gavanelli1 , Evelina Lamma1 , Paola Mello2 , and Paolo Torroni 2

1 ENDIF - University of Ferrara - Via Saragat, 1 - 44100 Ferrara, Italy.

{malberti|m gavanelli|elamma}@ing.unife.it

2 DEIS - University of Bologna - Viale Risorgimento, 2 - 40136 Bologna, Italy.

{pmello|ptorroni}@deis.unibo.it

The operational semantics is an abductive proof-procedure which builds on the IFF and is proven sound for a relevant class of programs. It has been implemented using Constraint Handling Rules and integrated in a Java-based system for hypothetical reasoning [Alberti et al., 2005].

However, in most applications, this distinction is not adequate to capture the dynamics of knowledge, as reasoning is confronted with an environment in evolution. It may turn out that some hypotheses gain or lose strength, as events happen in the world. For example, in the medical domain, where a kind of hypothetical reasoning is the diagnostic inference, we can model symptoms as observations and diseases as (not directly measurable) hypotheses: test results and new possibly upcoming symptoms, instead, are none of these, and should be interpreted as hypotheses confirmable by events.

An abductive derivation verifies a goal by using deduction as in logic programming, but also by possibly assuming that some abducibles are true. In order to have this process converge to a meaningful explanation, an abductive theory normally comes together with a set of integrity constraints IC, and it is required that hypotheses be consistent with IC.

In our extended framework, we distinguish between two classes of abducible literals: hypotheses, as classically understood, and expectations about events. Expectations can be "positive" (to be confirmed by certain events occurring), or "negative" (to be confirmed by certain events not occurring).

We propose a new language to define abductive logic programs with expectations, inspired to the IFF proof procedure [Fung and Kowalski, 1997], and whose semantics extends those of classical ALP. The language permits to express abducible hypotheses and expectations with variables and constraints. Within this new framework we can model and reason about a number of concrete application scenaria. Our framework permits, e.g., to reason about deadlines, and to express and correctly handle expectations with universal quantification: this typically happens with negative expectations ("The patient is expected not to show symptomQ at all times").

∗This work is partially funded by the Information Society Technologies programme of the European Commission under the IST2001-32530 SOCS Project, and by the MIUR COFIN 2003 projects Sviluppo e verifica di sistemi multiagente basati sulla logica, and La Gestione e la negoziazione automatica dei diritti sulle opere dell'ingegno digitali: aspetti giuridici e informatici.

2 Dynamic ALP

An ALP [Kakas et al., 1992] is a tuple 〈KB, IC,A〉 where KB is a logic program, A is a set of predicates called abducibles not defined in KB, and IC is a set of formulae called Integrity Constraints. An abductive explanation for a goal G is a set ∆ ⊆ A s.t. KB∪∆ |= G and KB∪∆ |= IC.

New dynamically upcoming events are encoded into atoms H(Descr [, Time]) where Descr is a ground term representing the event and Time is an integer representing the time at which the event happened. Such events are recorded into a set (called history, or HAP) containing H atoms. A Dynamic Abductive Logic Program (DALP) is a sequence of ALPs, each grounded on a given history. We will write DALPHAP to indicate the abductive logic program obtained by grounding the DALP with the history HAP. The history dynamically grows during the computation, as new events happen. 1

An instance DALPHAP of this framework can be queried with a goal G, that may contain both predicates defined in KB and abducibles. The abductive computation produces a set ∆ of hypotheses, partitioned in two sets: general hypotheses (∆A) and expectations (EXP), containing positive expectations (in the form of E(Descr[,Time]) atoms), and negative expectations (EN((Descr [, Time])) atoms).

Typically, expectations will contain variables, over which CLP constraints can be imposed. Variable quantification is existential in E expectations, and universal in EN expectations (unless the same variable is used outside of such expectation). Explicit negation can also be applied to expectations. 2 Constraints on universally quantified variables will be considered as quantifier restrictions. For instance, EN(p(X)), X > 0 has the semantics ∀X>0 EN(p(X)).

The declarative semantics for DALPHAP is based on its ground version, and considers CLP-like constraints as defined predicates. First, an abductive explanation should entail the goal and satisfy the integrity constraints:

1 The source of events is not modelled, but can be imagined as a queue.

2 For each abducible predicate A ∈ {E,EN}, the abducible predicate ¬A is implicitly defined, to represent the negation of A, together with the integrity constraint (∀X)¬A(X), A(X) → false.

where, as in the IFF proof procedure, the symbol |= stands for three valued entailment and Comp stands for completion.

Among the sets of expectations of an instance DALPHAP, we select the ones that are consistent with respect to expectations (i.e., the same event should not be both expected to happen and not to happen), and that are confirmed:

Definition 1 A set EXP is E-consistent iff for each (ground) term p: {E(p), EN(p)} ̸⊆ EXP. (3)

Given a history HAP, a set of expectations EXP is confirmed if and only if for each (ground) term p:

We write DALPHAP≈∆A∪EXPG if equations (1-4) hold.

The operational semantics is an extension of the IFF. Each state is defined by a tuple defining confirmed, disconfirmed, and pending expectations, along with the resolvent, the set of abduced literals that are not expectations, the constraint store, a set of partially solved integrity constraints, and HAP.

A derivation D is a sequence of nodes Tj , where the initial node T0 contains the goal G as the initial resolvent, and the other nodes Tj , j > 0, are obtained by applying one among a set of transitions, until quiescence.

Definition 2 Starting with an instance DALPHAPi there exists a successful derivation for a goal G iff the proof tree with root node T0 has at least one consistent leaf node Tn (i.e., there exists for Tn a ground variable assignment such that all the constraints are satisfied). In that case, we write:

The transitions are those of the IFF, enlarged with those of CLP, and with specific transitions accommodating the concepts of hypotheses confirmation and evolving history.

The CLP(FD) solver has been extended for dealing with universally quantified variables and quantifier restrictions. For instance, given two expectations ∀X<10EN(p(X)) and ∃Y>5E(p(Y )), the solver is able to infer ∃Y≥10E(p(Y )). To the best of our knowledge, this is the only proof-procedure able to abduce atoms containing universally quantified variables; moreover, it also handles constraints `a la CLP on universally quantified variables.

We proved soundness for allowed DALPs: 3

Theorem 1 Given DALPHAPi and a ground goal G, if DALPHAPi ∼HAP ∆ G then ALPHAP≈∆G.

3 Case study

We conclude with an example from the medical domain to show two main contributions of our work: the dynamic detection of new facts, and the confirmation of hypotheses by events. Suppose a symptom s can be caused by one of three types of diseases. Let disease d1 be an acceptable explanation for s if the patient is not also affected by d3, and in such a case the patient's temperature cannot go below 37oC. s may alternatively be caused by disease d2, and in this case red spots are expected to appear on the patient's skin within 4 days. Finally, d3 may be the cause of s, provided that an exam r gives a positive result:

3 The proof is based on a correspondence drawn between SCIFF and IFF transitions, and exploits the soundness results of the IFF.

The initial goal can be the observation symptom(s, 1). We model disease as a classical abducible, whereas expectations are used to corroborate the explanations.

Notice the twofold use of expectations: both in the second and third clause, the expectation defines a further event that can support the diagnosis. But while E(red spots, T2) simply defines the expected course of illness (in order for the diagnosis to be corroborated), E(exam(r, +), T1) can also be intended as a suggestion to the physician for a further exam to be done, or as a request of further information.

The combinations of abducible literals can be refined by means of ICs. For example, if the result of some exam r is positive, then we can assume that the patient is not affected by disease d1: H(exam(r, +), T1) → not disease(d1, T1). The dynamic occurrence of events can drive the generation and selection of abductive explanations. If the query is, e.g., symptom(s, 1), there can be three alternative explanations:

{disease(d1, 1), ∀T>37EN(tem(T ), 1)},

{disease(d2, 1), ∃1<T2≤5E(red spots, T2)}, and

{disease(d3, 1), E(exam(r, +), 1)}.

If event H(tem(36), 1) happens, the first set contains a disconfirmed expectation: ∀T>37 EN(tem(T), 1), so it can be ruled out. If, within the deadline T2 ≤ 5, the event red spots does not happen, the second set is excluded as well, and only the third remains acceptable.

Finally, integrity constraints could suggest possible cures, or warn about consequences of not taking certain drugs:

4 Conclusions

We presented SCIFF, an abductive proof-procedure able, beside proposing explanations, to infer expectations about the happening of events. Expectations are abducibles, but more expressive: they can contain universally quantified variables, possibly with CLP constraints. They can represent requests for information, or the expected evolution of a system. SCIFF is able to process dynamically incoming events to confirm the expectations, providing corroboration to abduced hypotheses.