Abduction in Concurrent Constraint Programming

Philippe Codognet INRIA-Rocquencourt Domaine de Voluceau 78153 Le Chesnay,

FRANCE

Philippe.Codognet@inria.fr

Vijay Saraswat Xerox PARC

3333 Coyote Hill Road Palo Alto, CA 94304,

U.S.A.

saraswat@parc.xerox.com

March 1992

Topic Area : Reasoning methods (deduction, abduction, constraint solving, belief revision)

Abstract

TBD

1 Introduction

Abduction was introduced by Pierce [1] as a new inference mechanism for logical systems along with deduction and induction. It has been used in various domains such as semiotics [2], linguistics [3], and in Artificial Intelligence, since [4], mainly in the perspective of diagnostic reasoning [5] [6] [7].^{1} Abduction has also been introduced in Logic Programming by [8], and then further developed in [9] [10] [11].

Although Constraint Logic Programming (CLP) languages have been introduced for some years [12] and generalize in an obvious way Logic Programming, no attempt have been made to extend abduction to such a framework, in spite of numerous analogies existing between abduction and constraint processing. Indeed both systems are intended to deal with partial information and to avoid floundering when dealing with under-specified problems, both in fact conjecture relations between unknowns instead of getting stuck in a “dead-end” when complete characterization is missing. This correspondence is stressed in that the basic step of an abduction process consist in adding an abducible literal to the current set of hypotheses as long as it is consistent with it, while the basic step of constraint solving consists in adding a new constraint to the current set of constraint and checking consistency.

Our work is intented to propose a notion of abduction for CLP languages, and more precisely for the family of Concurrent Constraint (cc) languages proposed by [15] [16], which extend CLP languages with concurrency features that have emerged from the domain of Concurrent Logic Programming. The key idea underlying the cc framework is to use constraints to extend the synchronization and control mechanisms of concurrent logic languages. Briefly, multiple agents (processes) run concurrently and interact by means of a shared store, i.e. a global set of constraints. Each agent can either add a new constraint to the store (Tell operation) or check wether or not the store entails a given constraint (Ask operation). Synchronization is achieved through a blocking ask : an asking agent may block and suspend if one cannot state if the asked constraint is entailed nor its negation is entailed. Thus nothing prevents the constraint to be entailed, but the store does not yet contain enough information. The agent is suspended until other concurrently running agents add (Tell) new constraints to the store to make it strong enough to decide.

The denotational semantics of cc languages [17] consists in interpreting the basic operations in cc languages and the agents as closure operators over the underlying constraint system ^{2}. A constraint system is a pair (D, ⊢) where D is the constraint domain and ⊢ an entailment relation over D satisfying some simple conditions, [17]. In this framework, abduction consists, given a constraint c, an agent a and a store s, to find a minimal explanation d of c, that is a constraint d such that a(s ∪ d) ⊢ c. This means that we want to find the minimal extension (d) of the current store s so that, running the agent a in the store s ∪ d, we could derive something equal or stronger than c, i.e. something with “at least as much information” as c. In general, a and s are given beforehand, and this scheme can be used for diagnostic reasoning as follows : the definition of the agent a is a program describing some artifact, s represent some internal integrity constraints. Then the constraint c represent some observation, and the explanation d corresponds thus to the “causes” of c given a, that is the constraint corresponding to the behavior hypotheses that that are necessary to derive an output constraint at least as strong as c (the observation).

1[more on abduction in AI (Poole,...)]

2A closure operator f over a lattice (L, ≤) is a unary function that is monotone (i.e., f(x) ≥ f(y) whenever x ≥ y), idempotent (i.e., f(f(x)) = f(x)) and extensive (i.e., f(x) ≥ x).

So what could be the operational behavior of such an abduction mechanism in the cc framework ? Intuitively, considering that abduction in deductive systems is a mean to generate hypotheses allowing the deduction process to continue when normally a “dead-end” is reached (cf. [5]), then by analogy abduction in cc languages should allow the computation to continue when a “deadlock” is reached, i.e. when all agents are suspended on some ask operations. Thus abduction has to generate some hypothetical constraints that would lead some ask operations to be satisfied and thus resume some agents in order to let the computation proceed again. Hence the abduction mechanism is intended to “abduce” the minimal input needed for an agent to resume and generate some new output. This scheme thus abduce ask operations upon which some agents are pending, telling then the “asked contraints” to some hypothetical sub-store.

The paper is organized as follows. Section 2 briefly presents the basic definitions of constraint systems and concurrent constraint (cc) languages. Section 3 introduces the concept of abduction in such a framework, and define the notion of explanation and minimal explanation. Section 4 then relates it to the operational behavior of cc languages, in order to give a concrete abduction procedure, whose equivalence w.r.t. the declarative notion is shown. In Section 5, we dicuss the problem of controlling such an abductive process, i.e. of controlling the generation of hypotheses. Section 6 proposes a simple application to diagnostic reasoning, and a short comparison with previous work on abduction is conducted in Section 7, followed by a short conclusion.

2 cc languages

The central concept underlying cc languages is that of a constraint system. Briefly, a constraint system is any system of partial information which comes equipped with notions of consistency and entailment. For the purposes of the present paper, we shall assume that such a constraint system L is specified by a certain set of first-order formulas, and the entailment relation ⊢between finite sets of formulas and single formulas is obtained by interpreting these formulas in a certain pre-specified class of models. (Thus c_{1}, …, c_{n} ⊢ c if in each model in this class, for all valuations for the free variables, c must be true, whenever each of the c_{i} are true.) More details and more general definitions may be found in [15] and [18]. In the following, for any finite set of variables V, we shall use the notation L(V) to indicate the set of constraints whose free variables lie in V.

The syntax of the non-determinate cc languages is very simple:

Programs P ::= H::A | P.P
Agents A ::= c  (Tell)
| c → A  (Ask)
| A, A  (Conjunction)
| A; A  (Disjunction)
| ∃XA  (Local variables)
| H  (Procedure Call)
Procedure Call H ::= p(X_{1}, …, X_{n})

(1)

Programs are just sequences of definitions, associating an atomic formula with an agent. An agent is either a primitive constriant, a simple conditional (ask) agent, an abducible ask agent, a conjunction (parallel composition), disjunction (backtracking search), existential quantification (local hiding), or atomic formula (procedure call).

We now discuss the operational semantics of cc languages. Configurations are pairs of the form ⟨Γ, s⟩ where s is a set of constraints, and Γ is a multiset of agents. (The empty multiset is denoted ().) Below, we define a binary relation ⟶, the transition relation which specifies how configurations evolve. Note that only fair execution sequences (e.s.) are considered legal. (A fair e.s. is not unfair; an unfair e.s. is one in which some given transition is enabled at every configuration in the sequence, and never taken.)

We omit the rules for existential quantification, backtracking and procedure calls, since they are standard. (See for example, [14].) Below, ⊢ is the entailment relation of the underlying constraint system.

\overline{⟨(Γ, c), s⟩ ⟶ ⟨Γ, s ∪ \{c\}⟩} (Tell)

\frac{s ⊢ d}{⟨(Γ, d → A), s⟩ ⟶ ⟨(Γ, A), s⟩} (Ask)
\overline{⟨(Γ, (A_{1}, A_{2})), s⟩ ⟶ ⟨(Γ, A_{1}, A_{2}), s⟩} (Parallel Composition)

(2)

The operational semantics of the cc languages has two abstract characterizations. The first is a logical characterization: in fact cc programs can be directly read as first-order formulas and it can be shown that the operational semantics of cc languages is sound and complete for first-order constraint entailment. This means the following. Say that A ⊧_{P} c iff in all first-order models of the given program (built on top of the given models of the constraint system), every valuation satisfying A satisfies c. Then we have that if ⟨A, ∅⟩ ⟶^{∗} ⟨Γ, c⟩, then A ⊧_{P} c and if A ⊧_{P} c then there is a Γ and a c′ such that ⟨A, ∅⟩ ⟶^{∗} ⟨Γ, c′⟩ and c′ ⊢ c [13].

The second characterization is more direct. Agents are given denotations as closure operators over the underlying constraint system. The operator corresponding to an agent is merely the operator that maps each input to the limit of all fair execution sequences of the agent on that input. It is not hard to show that, because of the monotonic nature of ask and tell operations, the operators thus generated are monotone, idempotent and extensive, that is, are closure operators.

Closure operators capture the essence of the notion of entailment: any set of inference rules can be associated with a closure operator which maps a set of formulas to their closure under the inference rules. Indeed closure operators were initially introduced by Tarski for precisely the purpose of characterizing the notion of logical entailment. It is rather remarkable that such a simple notion has turned out to provide a very simple natural and powerful mathematical interface between computation and logic (see, e.g., [17]). In particular, these operators enjoy a number of remarkable computational properties. The most important of these is that such operators can be completely characterized by the set of their fixed points — for, each input is mapped by such an operator to its least fixed point above that input. Indeed, a number of computationally important operations on closure operator have rather simple definitions in terms of sets of fixed points. For example, the parallel composition of two closure operators f and g corresponds logically to their conjunction, and yields a closure operator whose fixed points are precisely the intersection of the fixed points of f and g.

3 Abduction in cc languages

We begin by giving an abstract description of the notion of abduction in a setting in which computation and deduction are captured by the notion of closure operators over first-order constraint systems.

Definition 3.1 Let SD : L → L be a closure operator, and r ∈ L a constraint, and V a set of variables. A constraint e ∈ L(V) is an explanation for r if SD(e) is consistent and SD(e) ≥ r. We shall write e |⊢_{SD,V} r, and just e |⊢ r, when SD and V are clear from the context.

An explanation is minimal, if, in addition, for any other explanation e′, it is the case that e′ = e whenever e′ ≤ e.

Thus an explanation is an input which can explain the result (via the given the inference rules SD). Alternatively, the given inference rules f can be considered as transducers that transform a given output condition r to one of perhaps many input conditions i, in the variables V, such that if f is invoked in a store stronger than i, then the system is guaranteed to quiesce in a store stronger

Configurations are now tuples of the form ⟨Γ, s, d, V ⟩ where d is a set of (abduced) constraints, V the set of abducible variables, s is a set of constraints, and Γ is a multiset of agents.

\overline{⟨(Γ, c), s, d, V ⟩ ⟶ ⟨Γ, s ∪ \{c\}, d, V ⟩} (Tell)
\frac{s ∪ d ⊢ c}{⟨(Γ, c → A), s, d, V ⟩ ⟶ ⟨(Γ, A), s, d, V ⟩} (Ask)
\overline{⟨(Γ, (A_{1}, A_{2})), s, d, V ⟩ ⟶ ⟨(Γ, A_{1}, A_{2}), s, d, V ⟩} (Parallel Composition)

\frac{⟨(Γ, c → A), s, d, V)⟩ −̸→ s ∪ d ∪ c ⊬ false var(c) ⊆ V}{⟨(Γ, c → A), s, d, V ⟩ ⟶ ⟨(Γ, A), s, d ∪ c, V ⟩} (Abduction)

(3)

Table 1: Transition system for Abductive cc language

than r. A minimal explanation, is one which makes just as many assumptions as needed to obtain an explanation. The connections with Dijkstra’s (weakest) pre-conditions for imperative programs are obvious.

Clearly, there may be more than one explanation for a given SD, r and V. We have:

Proposition 3.1 Assume SD and V are fixed.

• d |⊢ r_{1} and d |⊢ r_{2} implies d |⊢ c_{1} ∧ c_{2}

• d |⊢ c and c ⊢ e implies d |⊢ e

• e |⊢ c whenever e ⊢ d, SD(e) < false, and d |⊢ c.

4 An operational abduction procedure

The operational semantics of the Abductive cc language is shown in Table 1.

The transition system for Abductive cc specifies how to compute explanations for agents. Below we discuss the connection between the abstract notion of explanation for closure operators, and the computational description provided by the operational semantics.

Definition 4.1 An abduction system α is a triple ⟨A, V, P ⟩, where A is a cc agent, V a set of abducible variables, and P a cc program.

For α such a system, we shall write |⊢_{α} for the relation |⊢_{f_{α},V}, where f_{α} is the closure operator generated by A and P.

Definition 4.2 An abduction system α = ⟨A, V, P ⟩ is said to generate an explanation d for e if there exists a Γ and c, such that:

⟨A, ∅, ∅, V ⟩ ⟶^{∗} ⟨Γ, c, d, V ⟩ −̸→

and d ∪ c is consistent, and d ∪ c ⊢ e.

Theorem 4.1 (Soundness of Abductive cc) If an abduction system α = ⟨A, V, P ⟩ generates the explanation d for e, then d |⊢_{α} e.

Theorem 4.2 (Completeness of Abductive cc) Let α = ⟨A, V, P ⟩ be an abduction system, and assume that d |⊢_{α} e. Then there exists a d′ such that α generates the explanation d′ for e, and d ⊢ d′.

In particular, note that for any abduction system α, every minimal explanation d for e is generable.

5 Controlling abduction

In order to be truly usable, hypothetical reasoning systems need adequate strategies for focusing the generation of hypotheses to useful parts of the search space and avoiding combinatorial explosion. This problem is crucial in Assumptionbased sytems (e.g. ATMS), see [21] [22] for such a discussion. More generally, this means that the abduction process has to be controlled in order to minimize abduction. Also it is important, as soon as some constraint has been abduced, to immediately resume deductions that use it in order to confirm or deny the hypothesis as quickly as possible. This amounts to a full hypothetico-deductive system in the spirit of [??evans91??].

In our framework, we can take advantage of the genuine concurrency of the model, to achieve such a behavior. All agents with asks pending on some abducible constraint (i.e. whose action is dependant of this hypothesis) will be woken up as soon as the constraint will be abduced and added to the store. To control abduction and achieve a lazy hypothesis formation policy, we can also take advantage of research on concurrent logic languages, such as the Andorra principle. The Andorra principle was proposed by D.H.D. Warren [24] in order to combine Or- and And-parallel execution of logic programs, and it has now bred a variety of idioms and extensions developed by different research groups, among which Andorra-I [25] and Andorra Kernel Language[26]. The essential idea is to execute determinate goals first and concurrently, delaying thus the execution of non-determinate goals until no determinate goal can proceed any more. The roots of such a concept can be traced back further to the early developments of Prolog, as for instance in the sidetracking search procedure of [??Pereira-Porto79??] which favors the development of goals with the least alternatives (and hence determinate goals as a special case). This is indeed but another instance of the old “first fail” heuristic often used in AI.

Applying such ideas to the abduction scheme, one could design a strategy that would delay abduction as long as normal (deductive) computation can execute. Abduction takes place only when normal computation reaches a deadlock and cannot proceed anymore without additional (hypothetical) information. Moreover, as soon as a constraint is abduced, i.e. added to the store, normal computation can resume following the usual cc operational semantics, until a new deadlock is reached and more hypothesis are demanded.

Focused search is thus very easily and smoothly integrated in the usual cc operational behavior, thanks to the concurrent execution mechanism and a simple variant of the Andorra principle.

6 Application to diagnostic reasoning

Our main application topic is diagnostic reasoning, and especially fault diagnosis, as most abductive systems in AI. In that direction it looks very interesting to investigate constraints over finite domains, as proposed by the CHIP constraint language [23]. Finite domains nicely fits into the cc framework, as shown by the cc(FD) language presented in [27]. We believe that such a language is well suited for diagnostic reasoning for two main reasons. First, because diagnostic problems hypotheses typically concern the faulty state of some components, and the set of all such possible state is in general (hopefully) finite. Second, because very efficient constraint solving algorithms exist for that domain, and we could thus hope to have an efficient diagnostic reasoner.

In the examples that follow, we assume implemented a top-level interface abduce(Agent, Vars, Conclusion) which takes a cc agent, a list of variables (and their names), and a set of constraints, and prints out the constraints in the specified variables that need to be assumed so that running Agent will produce

Conclusions.

The three bulbs example. Let us now now describle a simple fault diagnosis problem and its formulation in cc(FD). This example is rephrased from [28] and deals with a simple electrical circuit consisting of three bulbs connected in parallel to a battery by wires. Observation shows that only the third bulb is lit and an explanation of this phenomenon is sought.

battery(Mode, Left, Right) ::
    Mode = empty → (Left = 0, Right = 0),
    Mode = ok → (Left = plus, Right = plus).
wire(State, In, Out) ::
    State = ok → In = Out,
    State = broken → Out = 0.
bulb(State, Light, Left, Right) ::
    State = ok → (Left = plus, Right = plus → Light = on),
                 (Left = 0 → Light = off),
                 (Right = 0 → Light = off),
    State = damaged → Light = off.

circuit(S, B1, B2, B3, W1, W2, W3, W4, W5, W6, L1, L2, L3) ::
battery(S, Sl, Sr), wire(W1, Sl, B1l), wire(W2, Sr, B1r),
bulb(B1, L1, B1l, B1r), wire(W3, B1l, B2l), wire(W4, B1r, B2r),
bulb(B2, L2, B2l, B2r), wire(W5, B2l, B3l), wire(W6, B2r, B3r),
bulb(B3, L3, B3l, B3r).

With the predicate q/1 defined by:

q ::

L = [s − S, b1 − B1, b2 − B2, b3 − B3, w1 − W1, w2 − W2, w3 − W3, w4 − W4, w5 − W5, w6 − W6],
abduce(circuit([S, B1, B2, B3, W1, W2, W3, W4, W5, W6], O1, O2, O3), L,
       (O1 = off, O2 = off, O3 = on)).

we obtain the interaction:

| ?- q.
Explanation: b3=ok,w6=ok,w5=ok,b2=damaged,w4=ok,w3=ok,b1=damaged,w2=ok,w1=ok,s=ok,true.
yes
| ?-

Combinational circuits. More generally, it is possible to give system descriptions of combinatorial digital circuits in a straightforward way, in cc languages. In Abductive cc it is possible to obtain abductive diagnoses in a straightforward way.

gate(Id, Type, In1, In2, Out) ::
(Id = ok → table(Type, In1, In2, Out)),
(Id = stuck at 0 → Out = 0), (Id = stuck at 1 → Out = 1).
table(and, I1, I2, O) ::
(I1 = 0, I2 = 0 → O = 0), (I1 = 0, I2 = 1 → O = 0),
(I1 = 1, I2 = 0 → O = 0), (I1 = 1, I2 = 1 → O = 1).
table(or, I1, I2, O) ::
(I1 = 0, I2 = 0 → O = 0), (I1 = 0, I2 = 1 → O = 1),
(I1 = 1, I2 = 0 → O = 1), (I1 = 1, I2 = 1 → O = 1).
table(xor, I1, I2, O) ::
(I1 = 0, I2 = 0 → O = 0), (I1 = 0, I2 = 1 → O = 1),
(I1 = 1, I2 = 0 → O = 1), (I1 = 1, I2 = 1 → O = 0).
adder([Sx1, Sa1, Sx2, Sa2, So], In1, In2, In3, Out1, Out2) ::
gate(Sx1, xor, In1, In2, X1), gate(Sa1, and, In1, In2, A1), gate(Sx2, xor, X1, In3, Out1),
gate(Sa2, and, In3, X1, A2), gate(So, or, A1, A2, Out2).

With the predicate q/1 defined by:

q(L) ::

    L = [sx1 − Sx1, sa1 − Sa1, sx2 − Sx2, sa2 − Sa2, so1 − So1],
    Modes = [Sx1, Sa1, Sx2, Sa2, So1],
    abduce((adder(Modes, 0, 1, 0, Out1, Out2), adder(Modes, 1, 1, 1, Out3, Out4)),
          L, (Out1 = 0, Out2 = 0, Out3 = 1, Out4 = 1)).

we obtain the interaction:

| ?- q(A).
Explanation: so1=ok,sa2=ok,sx2=ok,sa1=ok,sx1=stuck_at_0,true.
yes
| ?-

7 Relations with other approaches

3

As ask operations corresponds to a simple form of intuitionistic implication [13], our abduction scheme relates to a system of hypothetical reasoning with implicative clauses such as [19].

Also remark that constraints are abducibles and not agents, which could seem quite away from the original paradigm of abduction in logic programs [8] where predicates are abducibles. However Kowalski’s scheme can be easily rephrased in our framework : it corresponds to the special case of the Herbrand constraint system, that is, in the traditional view of constraints as first-order formulas with domain-specific interpretations [12] [15], the constraint system where constraints are interpreted in their free algebra. Moreover the notion of “integrity constraints” in that scheme then straightforwardly correspond to have some initial set of constraints in our framework.

A scheme for integrating cc languages and hypothetical reasoning has already been proposed in [20] which integrates ATMS-based techniques in the cc approach. The main difference is its explicit handling of the assumptions underlying a constraint (in the ATMS manner), while our approach mainly deals with an implicit handling of assumptions. Assumptions are also limited in [20] to boolean constraints (as in the traditional ATMS), while any constraint domain can be used in the new scheme.

8 Conclusion

We have presented a general scheme for abduction in concurrent constraint (cc) languages, which truly relates abduction and constraint solving. Thanks to the generality of cc languages, it emcompasses both logic languages and CLP languages as particular instances. This approach can be smoothly integrated into the denotational semantics of cc languages. For control issues the genuine concurrency of the model, coupled with a variant of the Andorra principle for delaying abduction as long as normal (deductive) computation can proceed, are sufficient to provide a focused behavior and a lazy hypothesis formation policy.

3[More on AI approaches (Poole, ...)]

Acknowledgements.

References

[1] Charles S. Pierce. collected papers. Cambridge University Press, 1933.

[2] Umberto Eco. Semiotics and philosophy of language. 1984

[3] J. Hobbs, M. Stikel, P. Martin and D. Edwards. Interpretation as abduction. In proceedings of the 26th Annual Meeting, Association for Computational Linguistics, Buffalo, USA, 1988.

[4] H. E. Pople Jr. On the mechanization of abductive logic. In proceedings of IJCAI 73, 1973.

[5] P. T. Cox and T. Pietrzykowski. Causes for events : their computation and application. In proceedings of the 8th Conference on Automated Deduction, LNCS 230, Springer Verlag 1986.

[6] D. Poole. Explanation and prediction: an architecture for default and abductive reasoning. Canadian Computational Intelligence Journal, vol. 5 (2), 1989.

[7] Raymond Reiter and Johan de Kleer. Foundations of assumption-based truth maintenance systems: a preliminary report. In Proceedings of AAAI-87, pages 183 – 188, August 1987.

[8] K. Eshghi and R. A. Kowalski. Abduction through Deduction. Research report, Imperial college, March 1988.

[9] K. Eshghi and R. A. Kowalski. Abduction compared with negation as failure. In proceedings ICLP 89, Lisbon, Portugal, MIT Press 1989.

[10] A. C. Kakas and P. Mancarella. Generalized stable models : a semantics for abduction. In proceedings of ECAI 90, Stockholm, Sweden, 1990.

[11] A. C. Kakas and P. Mancarella. On the relation between truth maintenance and abduction. In proceedings of PRICAI 90, Nagoya, Japan, 1990.

[12] J. Jaffar and J-L. Lassez. Constraint Logic Programming. In POPL-87, Munich, FRG, January 1987.

[13] Patrick Lincoln and Vijay Saraswat. Proofs as Concurrent Processes: A Logical Interpretation for Concurrent Constraint Programming. Technical report, Systems Sciences Laboratory, Xerox PARC, November 1991.

[14] R. Jagadeesan, V. Shanbhogue, and V. Saraswat. Angelic non-determinism in concurrent constraint programming. Technical report, System Sciences Laboratory, Xerox PARC, January 1991.

[15] V.A. Saraswat. Concurrent Constraint Programming Languages. PhD thesis, Carnegie-Mellon University, 1989.

[16] V.A. Saraswat and M. Rinard. Concurrent Constraint Programming. In Proceedings of Seventeenth ACM Symposium on Principles of Programming Languages, San Francisco, CA, January 1990.

[17] V.A. Saraswat, M. Rinard, and P. Panangaden. Semantic Foundations of Concurrent Constraint Programming. In Proceedings of Ninth ACM Symposium on Principles of Programming Languages, Orlando, FL, January 1991.

[18] V.A. Saraswat. The category of constraint systems is Cartesian-closed. In Proceedings of the IEEE Symposium on Logic in Computer Science, Santa Cruz, Ca, June 1992.

[19] D. M. Gabbay. N-Prolog : an extension of Prolog with hypothetical implication. Journal of Logic Programming, vol. 1 (4) 1984 and vol. 2 (4) 1985.

[20] V. Saraswat, J De Kleer and B. Williams. In proceedings of ILPS workshop on defeasible reasoning and constraint solving, San Diego, USA, 1991.

[21] Forbus K. D. and de Kleer J. “Focusing the ATMS”, proceedings of the 7th National Conference on Artificial Intelligence, St Paul, 1988.

[22] P. Codognet and P. Savéant, A Metalanguage for Representation and Control in Assumption-based Problem Solvers , In 2nd International Conference on Software and Knowledge Engineering, Skokie, USA, 1990.

[23] P. Van Hentenryck. Constraint Satisfaction in Logic Programming. Logic Programming Series, The MIT Press, Cambridge, MA, 1989.

[24] D.H.D. Warren. The Andorra Principle. Presented at the 1987 GigaLips workshop, University of Bristol.

[25] Vítor Santos Costa, David H. D. Warren, and Rong Yang. The Andorra-I engine: A parallel implementation of the basic andorra model. Proceedings of the Eighth International Conference on Logic Programming, pages 825–839, MIT Press, 1991.

[26] Sverker Janson and Seif Haridi. Programming paradigms of the Andorra kernel language. Proceedings of the 1991 International Logic Programming Symposium, pages 167–186, MIT Press, 1991.

[27] P. Van Hentenryck, V. Saraswat and Y. Deville. Constraint processing in cc(FD). submitted for publication, 1991.

[28] P. Struss and O. Dressler. Physical negation - integrating fault models into the General Diagnostic Engine. proceedings of IJCAI 89, Detroit, 1989.

/*

A Abductive cc implementation

Authors Vijay Saraswat, Philippe Codognet

Bugs to: saraswat@parc.xerox.com,codognet@minos.inria.fr

Copyright: \begin{matrix}c \\ ◯ \end{matrix}Xerox Corporation, 1992, INRIA, 1992

This File: ab cc new.pl

Last Modified : Sun Mar 22 21:32:43 1992

Brief Description: The code in this file implements a top-level interpreter for abductive cc.

• Source programs are of the form:

                g::a.

where a (agents) is given by:

             a ::= true | g | c | c -> a  | a,a

‘,’ binds tighter than ‘->’.

• At this time constraints are given by:

           c ::= X=t | c,c

Richer constraints will be added subsequently.

• A top-level call is of the form:

            abduce(Sys, Vars, Conclusion)

Here Sys is an agent, Conclusion is a constraint, and Vars is a list of variables on which constraints can be abduced. Vars is a list each of whose entry is of the form Varname-Var, where Varname is a constant (the name of the variable). The list should associate at most one name for a variable. The system prints out the constraints abduced on these variables so that running Sys entails Conclusions. Multiple explanations are generated on backtracking.

• The algorithm used is the following:

– Initialize Assumptions to true.

– Run Sys as an agent, until it quiesces. Note that this will reduce an abducible agent if its ask condition is satisfied.

– If Conclusion is entailed stop, and print Assumptions.

– Otherwise check that the Conclusion is still consistent. If so, and there is an agent c -> a, with the constrained variables in c lying in the given set of variables, assume c, and continue with a added to the current quiescent system. When this fails, continue at (2) with the next abducible agent.

The algorithm will generate explanations, not minimal explanations. Minimization will be costly. Also, the same explanation may be generated multiple times, if there multiple derivations are possible.

Examples of the usage of this program are given in the files ex {3,4,5}.pl in this directory.

To run this program, just consult this file into Prolog, and the files that describe your input cc program.

Gotchas: There is no explicit syntax for existential quantification. Any variable occurring in the body of a definition g::a, and not occurring in the head, is automatically treated as an existential variable.

Also, disjunction (backtracking) is not supported in this implementation.

Exports: abduce/3.

Things to do: Augment with richer constraint. Think of compilation. How can information in the Conclusion be used to focus the search for assumptions? See the gotchas.

*/
:- op( 1200, xfx, ::).
abduce(B, Vars, Cons):- abduce(B, Vars, true, Cons).
abduce(B, Vars, Ass, Cons) :-
   run(B, NewB, true, Flag),
   (Flag == reduced
       -> abduce(NewB, Vars,  Ass, Cons)
       ; (ask(Cons)
             -> format("Explanation: ~p.~n", [Ass])
             ; (satisfiable(Cons),
                try_each(NewB, Vars, Ass, Cons)))).
try_each(((Abs -> Agent), Rest), Vars, Ass, Cons) :-
    (ass(Abs, Vars, Ass, Ass_1), call(Abs),
     abduce((Agent, Rest), Vars,  Ass_1, Cons)) ;
    try_each(Rest, Vars,  Ass, Cons).
run(true, NewB, B, _Flag):- !, NewB=B.
run(A=B, NewB, B, reduced) :- !, A=B, NewB=B.
run((Ask -> Agent), NewB, B, Flag) :- !,
     (ask(Ask)
        -> (Flag=reduced, run(Agent, NewB, B, _Flag))
        ; (satisfiable(Ask)
              -> NewB = ((Ask -> Agent), B)
              ;  NewB = B)).
run((G1, G2), NewB, B, Flag) :- !, run(G1, NewB, B, Flag), run(G2, B, B, Flag).
run(Goal, NewB, B, reduced) :- (Goal :: Agent), run(Agent, NewB, B, _Flag).
ass(true, _Vars, Ass, Ass).
ass((G1, G2), Vars, Ass, Res) :- ass(G1, Vars, Ass, A), ass(G2, Vars, A, Res).
ass((A=B), Vars, Ass, (Extname=B, Ass)) :- memchk(A, Vars, Extname).
satisfiable(Ask):- \+(\+(call(Ask))).
ask((A1, A2)):- ask(A1), ask(A2).
ask(A=B):- A==B.
memchk(A, [Name-B | _], Name) :- A == B, !.
memchk(A, [_| R], Name) :- memchk(A, R, Name).

/*

*/