Bottom-up Abduction by Model Generation

1 Introduction

Abduction, an inference to explanation, has recently been recognized as a very important form of reasoning for various AI problems that deal with commonsense knowl­ edge as well as scientific and engineering knowledge. For example, in diagnosis, plan recognition and design, when we observe the behavior of a system, we want to identify the hypotheses that can explain the observation. Also, in natural language understanding, sophisticated user in­ terfaces and communication among intelligent agents, it is recognized that an explanatory capability may play a crucial role [Charniak and McDermott, 1985]. One of the most popular formalizations of abduction in AI defines an explanation as a set of hypotheses that, if combined with the background theory, logically entails the given observed formula. This deductive-nomological view of abduction has enabled abduction to be implemented us­ ing deduction, in particular with resolution-based proof procedures. Along this line, there have been a number of resolution-based abductive systems [Pople, 1973; Cox and Pietrzykowski, 1986; Poole et al., 1987; Stickel, 1989; Demolombe and Farinas, 1991; Inoue, 1992].

· Address after April 1993: Department of Information and Computer Sciences, Toyohashi University of Technology, 1-1 Hibarigaoka, Tempaku-Cho, Toyohashi 441, Japan.

tcurrent address: Department of Information Engineer­ ing, University of Industrial Technology, 4-1-1 Hashimotodai, Sagamihara, Kanagawa 229, Japan.

t Address after April1993: Department of Computer Sci­ ence and Intelligent Systems, Faculty of Engineering, Oita University, 700 Daunoharu, Oita-shi, Oita 870-11, Japan.

Thus, we can expect that studies on automated ab­ duction may fill the gap between traditional, fast de­ ductive techniques and more advanced, AI-oriented com­ monsense reasoning. From the viewpoint of automated deduction and theorem proving, however, automated ab­ duction is a hard and challenging problem. This is be­ cause:

1. Abduction is not a proof-finding problem but a consequence-finding problem (see [Inoue, 1992]).
2. Usually, each abductive explanation is required to be consistent with the background theory. While consistency checking is expensive (undecidable in general), it is essential for some practical applica­ tions of abduction (design problems, for example) , since we are interested in systems that can reject inconsistent theories to obtain acceptable theories.

In this paper, we propose several techniques for imple­ menting abduction that use fast deductive techniques to realize fast abductive systems. In particular:

1. We provide new implementation methods for abduc­ tion using model generation theorem provers such as those in [Manthey and Bry, 1988; Fujita and Hasegawa, 1991]. Instead of finding some logical consequences of the given axioms, our methods gen­ erate some models of such formulas.
2. These methods are implemented in parallel on a parallel inference machine. Parallelization is an im­ portant source for realizing faster abduction.
3. Top-down, goal information is incorporated in these bottom-up procedures. This is an extension of the Magic Set method for deductive databases [Bancil­ hon et al., 1986; Bry, 1990] to deal with abduction.

We use the parallel model generation theorem prover MGTP [Fujita and Hasegawa, 1991] that is implemented in the parallel logic programming language KL1 [Ueda and Chikayama, 1990]. Since the MGTP can be used for both testing the ( un) satisfiability of an axiom set and generating the minimal models of a range-restricted ax­ iom set, every function necessary for abduction can be realized on it. To this end, we show two different program transformation methods each of which converts an ab­ ductive problem into a model generation problem. The basic idea behind such a transformation has also been employed to compute stable models [Gelfond and Lifs­ chitz, 1988] of general and extended (disjunctive) logic programs in [Inoue et al., 1992a].

This paper is organized as follows. In Sections 2 and 3, abduction and the MGTP prover are summarized. Sec­ tion 4 presents two realizations of parallel abductive sys­ tems using the MGTP. In Section 5, we evaluate these systems by applying them to a logic circuit design prob­ lem. Some extension of the presented abductive systems and related work are discussed in Section 6.

2 Abduction

The definition of abduction we consider here is similar to that proposed in [Poole et al., 1987]. An abductive framework is a pair (E, r), where Eisa set of formulas (the background theory) and r is a set of literals (the hypotheses or abducibles) . Let G be a closed formula (the goal). A set E of ground instances of r is an explanation of G from (E, r) if

1. E U E f= G, and

2. E U E is consistent.

An explanation of G is minimal if no proper subset E' of E is an explanation of G.

The computation of explanations of G from (E, r) can be seen as an extension of proof-finding by introducing a set of hypotheses from r that, if they could be proved by preserving the consistency of the augmented theo­ ries, would complete the proof of G. Alternatively, ab­ duction can be characterized by a consequence-finding problem [Inoue, 1992], in which some literals are allowed to be hypothesized (or skipped) instead of being proved, so that new theorems consisting of only those skipped literals are derived at the end of deductions instead of just deriving the empty clause. In this sense, abduc­ tion can be implemented by an extension of a top-down, backward-chaining theorem-provine; procedure. For ex­ ample, Theorist [Poole et al., 1987] and SOL-resolution [Inoue, 1992] are extensions of the Model Elimination theorem proving procedure [Loveland, 1978].

However, there is nothing to prevent us from using a bottom-up procedure to implement abduction. In fact, we have developed an abductive reasoning system called APRJCOT/0 [Ohta and Inoue, 1990], which consists of a forward-chaining inference engine and an ATMS [Reiter and de Kleer, 1987]. The ATMS is used to keep track of the results of inference in order to avoid both repeated proofs of subgoals and duplicate proofs on different hy­ potheses deriving the same subgoals.

Thus, the two reasoning architectures, top-down and bottom-up, are complementary, yet both have merits and demerits for computing abduction. As Inoue [1992] pointed out, SOL-resolution is direct in the sense that it is both sensitive to the given goal clause and re­ stricted to searching only those formulas consisting of candidate hypotheses only. However, top-down reason­ ing may result in redundant proofs of subgoals. On the other hand, bottom-up reasoning eliminates redundancy, while it may prove subgoals unrelated to the proof of the given goal.

These facts suggest that it is promising to simulate top-down reasoning using a bottom-up reasoner, or to utilize cached results in top-down reasoning. The former simulation has been proposed for definite Horn databases as the Magic Set [Bancilhon et al., 1986] or upside-down meta-interpretation [Bry, 1990] methods. As Stickel [1991] argues, this approach is better for abduction than the simulation of bottom-up reasoning by a top-down reasoner. This is because caching is more complicated and less effective for abduction since the search space for abduction is lar~er than that for deduction. There­ fore, [Stickel, 1991] attempts the upside-down meta­ interpretation approach for abduction for Horn and non­ Horn clauses. While Stickel does not consider the consis­ tency of abductive explanations in his procedure, his ap­ proach has been extended to abduction for Horn clauses by incorporating consistency checking for a parallel ver­ sion of APRICOT/0 in [Ohta and Inoue, 1992].

3 MGTP

This section outlines the model generation theorem prover MGTP [Fujita and Hasegawa, 1991; Inoue et al., 1992a] on which our parallel abductive systems are based. The MGTP is a parallel and refined version of SATCHMO [Manthey and Bry, 1988], which is a bottom­ up model generation theorem prover that uses hyperres­ olution and case-splitting on non-unit derived clauses.

Each clause in an axiom set E input to the MGTP is expressed in the form:

where Ai's (1 S i S m; m 2 0) and Cj,z's (1 S j S n, 1 S l S kj; kj 2 1; n 2 0) are atoms, and all variables are assumed to be universally quantified at the front of the clause. Clause (1) represents the formula (A1 /\ .. . I\ Am) :::> ((C1,1 1\ ·.· I\ C1,k,) V ... V (Cn,l 1\ ... I\ Cn,k..)) in the standard notation of first-order logic. The left­ hand side of -+ is called the antecedent of the clause, while the right-hand side is called the consequent of the clause. When n = 0, the clause A1, ... , Am -+ is called a negative clause and means that whenever a ground instance of A1/\ .. . I\ Am is true, there is a contradiction. When n = 1 and k1 = 1, the clause A1, ... , Am -+ C1,1 is called a definite clause. A Horn clause is either a definite clause or a negative clause.

In the following, an interpretation is defined as a set of ground atoms as usual, and is often called a model can­ didate. Given a current set M of model candidates, the MGTP applies the following operations to every model candidate ME M and generates the new set M':

1. (Model candidate rejection) If there is a nega­ tive clause of the form:

and a substitution u such that M I= (At 1\ ... 1\ Am)u, then M is discarded.

1. (Model candidate extension) If there is a non­ negative clause of the form:

and a substitution u such that M I= (At/\ .. . 1\Am)u and M ~ (Ci,t 1\ ... I\ Ci,k; )u for all i = 1, ... , n, then M U { Ci,t u, . .. , Ci,k; u} is in M' for every i = 1, .. . ,n.

3. Otherwise, M is in M'.

Here, we call the process of obtaining a substitution u a conjunctive matching of the antecedent against elements in M . This process does not need full unification if ev­ ery clause is range-restricted [Manthey and Bry, 1988), that is, if every variable in the clause has Its occurrence in the antecedent. In this case, since every model can­ didate constructed by the MGTP contains only ground atoms, it is sufficient to consider matching instead of full unification. The MGTP also improves efficiency by re­ moving redundant conjunctive matching with a ramified­ stack algorithm [Fujita and Hasegawa, 1991].

In the following, we assume that function symbols in the language are only constants and that the number of constants is finite. Given a set E of clauses and the initial set of model candidates Mo = {0}, the MGTP applies the above two operations to Mo and generates M t· This process is repeated as long as M n+ t =I M n holds. If the MGTP cannot apply any operation to some model candidate set Mo (that is, Mo is closed under the above two operations), it stops and returns M 0 · If Mo = 0, every model candidate has been rejected so that E is unsatisfiable. Otherwise, since each interpretation M E Mo satisfies every ground clause from E, M is a model of E. For example, if E consists of the four clauses:

then using the MGTP we get: Mo = {0}, Mt = {{R(A)}}, M2 = {{R(A),S(A)}}, M3 = { {R(A), S(A), P(A)}, {R(A), S(A), Q(A)} }, and M4 = { {R(A), S(A), P(A)}} =Mo. Now, let us denote the set of minimal (in the sense of set inclusion of atoms) model candidates from M as min(M). Then, the set of minimal models of E can be precisely given by min(Mo) [Inoue et al., 1992a; Inoue and Sakama, 1993].

4 Abduction by Model Generation

Here, we introduce two realizations of abductive reason­ ing systems built on the MGTP.t Figure 1 illustrates the abstract architecture for these systems. We consider the first-order abductive framework (E, r), where Eisa set of range-restricted Horn clauses and r is a set of atoms ( abducibles). Each abductive system first transforms the given abductive framework (E, r) into a set of clauses in a suitable form. Then, the MGTP is used for both (a) Model Generation of the transformed formulas and (b) Consistency Checks of some set of formulas augmented with hypotheses. These two functions correspond to the two conditions for each explanation E of G from (E, r) defined in Section 2: (i) E U E I= G and (ii) E U E is consistent. Here, we convert the problem of finding E by (i) to some model generation problem (a). In this case, since E is a set of Hom clauses, each set E U E for any E from r is a set of Horn clauses and has a unique minimal model. In this way, the problem of finding explanations of G can be reduced to that of finding models of E that satisfy G. The MGTP, thus, outputs every model M of the transformed clauses such that M contains a minimal explanation of the given goal.

1 We have also developed several parallel abductive sys­ tems using the MGTP other than the two described in this paper. See [Inoue et al., 1992b].

The two abductive systems below differ in how they transform the abductive framework (E, r). The first one, the MGTP+MGTP method, is a co-operative system in which Model Gene1·ation and Consistency Checks com­ municate with each other. The second one, the Skip method, on the other hand, does not separate Model Generation from Consistency Checks, but expands some model candidates while pruning others. Both methods are natural extensions of standard model generation for deduction to model generation for abduction.

4.1 MGTP+MGTP

The MGTP+MGTP method is illustrated in Figure 2. In this method, two kinds of MGTP's are combined: one MGTP is used for Model Generation, and the other MGTP's are used for Consistency Checks. Then, MGTP1 works as a forward-inference engine, while MGTP-2 only tests the (un)satisfiability of the given axioms. In this system, each hypothesis H in r is represented by fact(H, {H} ), and each definite clause in E of the form:

is transformed into a Hom clause of the form:

where Ei is a set of hypotheses from r on which Ai depends, and the function cc is defined as:

Especially, a positive unit clause -+ C is transformed to -+ fad(C, 0). In this case, since each transformed clause is a Horn clause, a global model candidate M is maintained as a unique model candidate in M at every stage of computation. M contains a set of atomic for­ mulas in the form of fad( A, E) that represents a meta­ statement that E U E f= A, and is stored in MGTP-1. Each time MGTP-1 derives a new ground atom, the con­ sistency of the combined hypotheses is checked by calling an MGTP-2. 2 Notice that MGTP-1 never uses any nega­ tive clause in E for Model Generation.

In MGTP-2, each clause of E is used as is, and, in par­ ticular, the negative clauses are necessary. This MGTP is used just for Consistency Checks, and whenever a set of hypotheses E is received, it tries to find a model of E U E. If a model is found then it returns E itself, else returns nil, which is a code for eliminating the derived fad. Note that even when E U E is consistent we do not have to generate all of its minimal models.

The parallelism in this method comes from calling multiple MGTP-2's at once. However, since every trans­ formed clause is Horn, no case-splitting occurs so that MGTP-1 may not be parallelized. Therefore, the effect of parallelization depends heavily upon how much consis­ tency checking can be performed in parallel at once.

4.2 Skip

No matter how good the MGTP+MGTP method might be, the system consists of two different components. The possibilities for parallelization therefore remain limited. In contrast, the Skip method does not separate the in­ ference engine from consistency checking, but realizes both functions in only one MGTP. In this method, the MGTP is used not only as an inference engine but also as a "generate-and-test" mechanism so that consistency checking is automatically performed. We can utilize the capability supplied by the MGTP to extend and re­ ject model candidates. Therefore, multiple model can­ didates can be kept in distributed memories instead of keeping a single, global model candidate M as in the MGTP+MGTP method. Thus, a. great amount of OR­ parallelism induced by case-splitting can be obtained.

2 Note that transformation (2) is similar to the method proposed by Stickel [1991], except that we additionally con­ sider the function cc for consistency checking.

The most direct way to implement reasoning with hy­ potheses is as follows. For each hypothesis H in r, we supply a clause of the form:

where -,KH means that "H is not assumed to be true in the model". Namely, each hypothesis is assumed either to hold or not to hold. Note here that we consider each literal -,K H not as a new formula in a suitable modal logic, but as a newly introduced atom in a program, hence we are still within the classical first-order logic. Then, for dealing with -,KH, we need the axiom schema:

The above schema is an integrity constraint saying that H cannot be true and disbelieved at the same time. In this way, each model candidate containing both H and -,KH is rejected.

The above technique, however, may generate 21r1 model candidates, and is, therefore, often explosive for a number of practical applications. To reduce the number of generated model candidates as much as possible, we can use a method that delays case-splitting for each hy­ pothesis. 3 That is, we do not supply any clause of the form (3) for any hypothesis of r, but, instead, introduce hypotheses when they are necessary. When abducibles H 1, ... , H n ( n ~ 0) from r appear in the antecedent of a Horn clause in E as:

we transform this clause into a non-Horn clause:

In this transformation, each hypothesis Hj in the an­ tecedent is shifted to the right-hand side of the clause in the form of -,KHj. Moreover, each Hj is skipped instead of being resolved, and is added to consequent C of the rule since C becomes true whenever all A/s and H/s are true. This operation is a bottom-up counterpart of the Skip & Cut rule in the top-down approach defined for SOL-S resolution in [Inoue, 1992, Section 5.2]. Just like the transformation in (3), we need to supply the schema ( 4) for the Skip method. For example, suppose that E consists of the clauses:

and the a.bducibles are r = { Cold(x), Hayfever(x) }. Then, (E, r) is transformed to the following clauses ~ by the Skip method:

3 The basic ideas behind the schema ( 4) and the delayed approach was first proposed for the processing of negation as failure with the MGTP in [Inoue et al., 1992a].

Let G = Sneeze( Tom) be the observation. Using the MGTP, two minimal models containing G are obtained from~ as:

By extracting the abducibles from Mt and Mz, we can get the two explanations of G, Et = { Cold ( Tom)} and Ez = { H ayfever( Tom)}.

4.3 Upside-Down Meta Interpretation for Abduction

As discussed in Section 2, bottom-up abductive systems can enhance their efficiency by incorporating the goal in­ formation and by simulating top-down reasoning. Here, we present two program transformation methods based on upside-down meta-interpretation ( UDM) approaches defined by [Bry, 1990; Stickel, 1991]. We first apply such a UDM transformation to the input clauses E, generat­ ing E', then further transform (E', r) by using a trans­ formation for the MGTP+MGTP method or the Skip method defined in previous subsections.

The first transformation, called the simple UDM transformation, transforms each definite clause of E in the form:

into the clauses:

In this method, the MGTP operations are applied for clause (6) only when goal(C) is present. Further, goal(C) invokes the subgoals of (6) by deriving every goal(Ai)· Thus, top-down reasoning is s~mulated in a breadth-first manner.

For each negative clause At, ... , Am -+ in E, we can apply the above transformation used for definite clauses. Then, since the consequent of a negative clause is empty, we supply -+ goal(Ai) for every Ai. This means that any subgoal in every negative clause is evaluated. How­ ever, as Ohta and Inoue [1992] pointed out, many nega­ tive clauses are irrelevant to finding explanations of the given goal from the abductive framework in general. If we evaluate all the subgoals in all negative clauses, the UDM method cannot achieve speedups compared with non-controlled bottom-up abduction. To overcome this difficulty, we restrict the evaluation of negative clauses to those clauses relevant to the goal by using the abstracted dependency analyzer [Ohta and Inoue, 1992] that ana­ lyzes logical dependencies between the goal and negative clauses at the abstract (e.g. , predicate symbol) level.

The second transformation, called the left-to-right UDM transformation, simulates top-down reasoning in such a way that for clause (6) each subgoal goal(Ai+t) ( 1 ~ i ~ m - 1) is invoked only after the previ­ ous subgoals goal(At ), ... , goal(Ai) have been solved. Thus, this method simulates ordered-linear resolution in a depth-first manner. In this method, each clause of

[Notation]

T:

R:

PEs:

T / R(PEs)

The smallest execution time (sec)

The speedup ratio ofT to the time obtained with a single PE (times)

The number of PEs used when Tis obtained (number)

form (6) is transformed to:

where k is the identifier of each clause C in E, and contk,i(V) keeps the obtained substitutions V for the variables appearing in At, ... , Am. As in the simple UDM transformation, the abstracted-dependency anal­ ysis is also employed for evaluating negative clauses in this transformation.

5 Evaluation

This section presents an evaluation of two abductive sys­ tems, the MGTP+MGTP method and the Skip method, by applying them to a design problem. The problem is to design a logic circuit that calculates the greatest common divisor (GCD) of two integers expressed in eight bits by using the Euclidean algorithm [Maruyama et al. , 1988]. The solutions are those circuits satisfying the given con­ straints on the basic cell count and delay time (the area­ time limit). There are several kinds of knowledge on the design of circuits (about 120 clauses): datapath design knowledge (i.e., how to construct a GCD circuit by com­ bining components) at the top level, component design knowledge (e.g., a subtractor can be constructed from the combination of a one's complement circuit and an adder) at the next level, and technology mapping rules (e.g., an adder can be constructed from a series of some CMOS standard cells) at the low level. The problem can be represented as abduction, in which we assume that some combination of components may satisfy all con­ straints. Thus, if hypotheses derive a contradiction with Speedup (times)

the background knowledge, we see that the sub-design violates some constraints.

Table 1 shows the experimental result of two abduc­ tive systems at run time on the PIM/m parallel infer­ ence machine developed at ICOT. The area-time limits are set in three ways (300-40ns, 400-50ns and 500-60ns). In order to evaluate two UDM methods, we also solved a subproblem (the design of subtractors) of the entire problem (the design of GCD circuits). 4

As shown in the table, the run time for designing sub­ tractors in each system is, as expected, much shorter than that for designing GCD circuits, since the reason­ ing is directed to the given subgoal. However, for the Skip method, the simple UMD transformation works better than the left-to-right UDM transformation, indi­ cating that the left-to-right simulation of top-down rea­ soning increases the sequential processing more than the breadth-first manner.

4 ln order to avoid possible combinatorial explosion caused by generating many redundant model candidates contain­ ing non-minimal explanations, we introduced some negative clauses that can be generated automatically by analysis in the Skip method. See [Inoue et al., 1992b] for details.

Figure 3 shows the run time graph for the design of GCD circuits with a 500-60ns limit, which is obtained by varying the number of available processor elements (PEs) between 1 and 64 on PIM/m. Figure 4 displays the speedup ratio for the same· problem when running two abductive systems. All reasoning tasks split with disjunctions are automatically allocated to the available number of processors. As shown in these figures, the Skip method provides better parallelism as well as faster abductive reasoning than the MGTP+MGTP method.

6 Final Remarks

We have presented several new program transformation techniques for fast, parallel and bottom-up abduction. First, we have converted the Horn abductive problem with consistency checking into model generation prob­ lems in two ways. Second, we have applied the two kinds of upside-down meta-interpretation transforma­ tions to abduction to incorporate top-down information. Although we need to further investigate how to avoid possible combinatorial explosion in constructing model candidates for the Skip method, we conjecture that the Skip metho~ will be the most promising from the view­ point of OR-parallelism.

For related work on computing abduction using a model generation theorem prover, Denecker and De Schreye [1992] recently proposed a proof procedure for object-level abduction defined in [Console et al., 1991]. Their abduction does not consider the consistency of ex­ planations. But, in contrast to us, they compute the models of the only-if part of a completed program that is not range-restricted in general even if the original def­ inite clauses are range-restricted. To this end, they have to extend the model generation method by incorporating complex term rewriting techniques, while we can use the original MGTP without change in the Skip method.

While we restricted the abductive framework (E, r) to a pair of Horn clauses and atomic abducibles, we can consider an extension of abduction which captures non­ monotonic and default reasoning. Then, another impor­ tant advantage of the Skip method is that it may eas­ ily be combined with negation as failure so that knowl­ edge bases can contain both abducibles and negation-as­ failure formulas as in the framework of [Kakas and Man­ carella, 1990]. This extension of the abductive frame­ work by incorporating negation as failure is formally dis­ cussed in [Inoue and Sakama, 1993].

Finally, efforts should be also devoted to investigat­ ing extensions of bottom-up first-order abduction to deal with non range-restricted, non-Horn clauses and literal abducibles, which can be dealt with by a top-down ap­ proach like SOL-resolution [Inoue, 1992] . An example of bottom-up abduction for non-Horn clauses without con­ sistency checking can be found in [Stickel, 1991], which uses contrapositives in the form of definite clauses. This technique may be incorporated for the MGTP+MGTP

method with consistency checking. One difficulty lies in the fact that, since the definite transformation using the meta predicate fact does not involve any case-splitting as is the case in the MGTP+MGTP method, it needs AND-parallelism [Hasegawa et al., 1992] for speed-up.

Acknowledgment

We wish to thank Mark Stickel and Franc,;ois Bry for useful comments on earlier work. We would also like to thank all the members of ICOT PAB (Parallel Abduc­ tion) Working Group for discussions on this work.