Consequence-Finding Based on Ordered Linear Resolution

1 Introduction

It is well known in automated deduction that while res­ olution [Robinson, 1965] is complete for proof-finding (called refutation complete), that is, it can deduce false from every unsatisfiable set of formulas, it is not deduc­ tively complete for finding every logical consequence of a satisfiable set of formulas. Lee [1967] addresses him­ self to this problem and defines the consequence-finding problem, which is expressed in the following form:

Given a set of formulas T and a resolution pro­ cedure P, for any logical consequence D ofT, can P derive a logical consequence C ofT such that C subsumes D?

If a resolution procedure is complete for consequence­ finding, then it is useful in spite of lacking deductive completeness because in general the logical consequences not deducible from the theory are neither interesting nor useful. Namely, such a formula is subsumed by some formula deducible from the theory and thus it is weak.

Historically, consequence-finding had been investi­ gated intensively since the resolution principle [Robin­ son, 1965] was invented for proof-finding. Lee's [1967]

completeness theorem was proved for the ori~nal reso­ lution principle. Slagle, Chang and Lee [1969J extended the result to various kinds of semantic resolution. How­ ever, after Minicozzi and Reiter [1972] extended these results to various linear resolution strategies in the early 70s, consequence-finding was once abandoned in research of automated theorem proving and attention has been directed towards only proof-finding 1 . It appears that there are three reasons for this discouragement:

1. The results presented by [Minicozzi and Reiter, 1972] are in some sense negative. Linear resolution involving C-ordering [Loveland, 1978; Reiter, 1971; Kowalski and Kuhner , 1971; Chang and Lee, 1973; Shostak, 1976] (literals are ordered in each clause in the theory), which is the most familiar and effi­ cient class of resolution procedures, is incomplete for consequence-finding. Thus, the completeness result that we would most like to obtain does not hold.
2. It is neither practical nor useful to find all of the consequences in general. However, there has not been an intellectual method which directly searches interesting formulas, instead of getting all theorems and then filtering them by some criteria.
3. As opposed to proof-finding, consequence-finding has lacked useful applications in AI.

In this paper, we re-evaluate consequence-finding and give new perspectives. The proposals are motivated and justified by the following solutions to the above three problems:

1. Recently, Finger [1987] gave a complete procedure based on set-of-support deduction for generating formulas (called ramification) derivable from a the­ ory and a newly added formula as an initial set of support. We provide a complete procedure for consequence-finding, which contains more restric­ tion strategies than Finger's, by adding one rule called skip operation to C-ordered linear resolution.
2. Bossu and Siegel [1985] give a complete algorithm for finding the set of positive clauses derivable from a groundable theory (called characteristic clauses).

1 0ne can see that textbooks of resolution-based theorem proving, such as [Chang and Lee, 1973; Loveland, 1978], have no sections for consequence-finding.

Recently, Siegel [1987] redefined the notion of char­ acteristic clauses for propositional theories and pro­ posed a complete algorithm for finding them. We show how our results can both improve the efficiency of Bossu and Siegel's algorithm and lift Siegel's for the general case. Moreover, easy modifications of the proposed procedure can be shown to be applied to more efficient variations of consequence-finding.

1. Przymusinski [1989] defines MILO-resolution to be used in his query answering procedure for circum­ scription of ground theories. MILO-resolution can be characterized as C-ordered linear resolution with skip operation [Inoue and Helft, 1990]. On the other hand, most procedures for abduction [Pople, 1973; Cox and Pietrzykowski, 1986; Finger, 1987; Poole, 1989; Stickel, 1990] can utilize consequence-finding procedures to generate explanations [Inoue, 1990]. We show how the proposed procedure can be applied to generate such interesting formulas for nonmono­ tonic and abductive reasoning. In the propositional case, the technique can be viewed as an elegant algo­ rithm to compute prime implicantsjimplicates, and thus can be utilized for the clause management sys­ tem [Reiter and de Kleer, 1987] that is a generaliza­ tion of the ATMS [de Kleer, 1986].

The importance of the results presented lies in their ap­ plicability to a wide class of AI problems. In other words, the methods shed some light on better understanding and implementation of many AI techniques.

The present paper is organized as follows. The next section characterizes consequence-finding in a general way, and shows how various AI problems can be well de­ fined by using this notion of characteristic clauses. Sec­ tion 3 presents the basic procedure, which is sound and complete for characteristic-clause-finding, based on C­ ordered linear resolution. Efficient but incomplete varia­ tions of the basic procedure and their properties are pro­ vided in Section 4. Because of space limitation, proofs of propositions are given in the full paper.

2 Characterizing Consequence-Finding

We define a theory as a set of clauses, which can be iden­ tified with a conjunctive normal form (CNF} formula. A clause is a disjunction (possibly written as a set) of liter­ als, each of which is a possibly negated atomic formula. Each variable in a clause is assumed to be universally quantified. For a method convertin~ a formula to this form of theory, see [Loveland, 1978J. If S is a set of clauses, by S we mean the set formed by taking the nega­ tion of each clause inS. The empty clause is denoted by D. A clause Cis said to subsume a clause D if there is a substitution (} such that CO C D and C has no more literals than D 2 . For a set of clauses E, by JJE or fJ [E] we mean the set of clauses of E not subsumed by any other clause of E. A clause C is a theorem, or a (logical) consequence of E if E f= C. The set of theorems of E is denoted by Th(E).

2 This definition of subsumption is called 8-1ubsumption in [Loveland, 1978]. Unlike in the propositional case, the second condition is necessary because a. clause implies its factor.

2.1 Characteristic Clauses

We use the notion of characteristic clauses, which is a generalized notion of logical consequences and helps to analyze computational aspects of many of AI prob­ lems. The idea of characteristic clauses was intro­ duced by Bossu and Siegel [1985) for evaluating a kind of closed-world reasoning and was later redefined by Siegel [1987] for propositional logic. The description below is more general than [Bossu and Siegel, 1985; Siegel, 1987; Inoue, 1990] in the sense that the notion is not limited to some special purposes and that it deals with the general case instead of just the propositional cases. Also, these notions are independent of implemen­ tation; we do not assume any particular resolution proce­ dure in this section. Informally speaking, characteristic clauses are intended to represent "interesting" clauses to solve a certain problem, and are constructed over a sub-vocabulary of the representation language.

Definition 2.1 (1) We denote by n the set of all pred­ icate symbols in the language. For R ~ n, we denote by R+ (R-) the positive (negative) occurrences of pred­ icates from R in the language. The set of all atomic formulas is denoted as A = n+, and the set of literals is denoted C = A u A = n + u n-.

(2) A production field Pis a pair, (Lp,Cond}, where Lp (called the characteristic literals) is a subset of C, and Cond is a certain condition to be satisfied. When Cond is not specified, P is just denoted as ( Lp }. The production field ( C} is denoted P c.

(3) A clause C belongs to a production field P = ( Lp, C ond} if every literal in C belongs to Lp and C satisfies Cond. The set of theorems of E belonging toP is denoted by Thp(E).

( 4) A production field P is stable if for any two clauses C and D such that C subsumes D, it holds that if D belongs to P, then C also belongs to P .

Example 2.2 Examples of stable production fields.

(1) P1 = Pc: Thp 1 (E) is equivalent to Th(E). (2) P2 =(A}: Thp 2 (E) is the set of positive clauses implied by E. (3) Pa = (A, size is less than k} where A ~ A:

T hp 3 (E) is the set of negative clauses implied by E con­ taining less than k literals all of which belong to A.

Example 2.3 P4 = (A, size is more than k} is not stable. For example, if k = 2 and p(a),q(b),r(c) E A, then D1 = p(a) V q(b) subsumes D2 = p(a) V q(b) Vr(c), and D2 belongs to P4 while D1 does not.

Definition 2.4 (Characteristic Clauses) Let E be a set of clauses, and P a production field. The character­ istic clauses of E with respect toP are:

Carc(E, P) contains all the unsubsumed theorems of E belonging to a production field P. To see why this no­ tion is a generalization of consequence-finding, let P be Pc. From the definition of consequence-finding, for any clause D E Th{E), a complete procedure P can derive a clause C E Th{E) such that C subsumes D. There­ fore, P can derive every clause C' E fJ Th(E) because C' is not subsumed by any other theorem of E. Hence, Carc(E, 'Pc.) = pTh(E) must be contained in the theo­ rems derivable from E by using P. Note also that the empty clause belongs to every stable production field 'P, and that if E is unsatisfiable, then Carc(E, 'P) contains only D. This means that proof-finding is a special case of consequence-finding. Next is a summarizing proposition.

Proposition 2.5 Let E be a theory, 'P a stable produc­ tion field. A clause D is a theorem of E belonging to 'P if and only if there is a clause C in Carc(E, 'P) such that C subsumes D. In particular, E is unsatisfiable if and only if Carc(E, 'P) = {D}.

As we will see later, when new information is added to the theory, it is often necessary to compute newly derivable consequences caused by this new information. For this purpose, consequence-finding is extended to look for such a ramification of new information.

Definition 2.6 (New Characteristic Clauses) Let E be a set of clauses, 'P a production field, and F a for­ mula. The new characteristic clauses ofF with respect to E and 'P are:

In other words, C E N ewcarc(E, F, 'P) if: (i) EU{ F} ~ C, (ii) C belongs to 'P, (iii) E ~ C, and (iv) no other clause subsuming C satisfies (i)-(iii).

The next three propositions show the connections be­ tween the characteristic clauses and the new characteris­ tic clauses. Firstly, N ewcarc(E, F, 'P) can be represented by the set difference of two sets of characteristic clauses.

Proposition 2. 7

When F is a CNF formula, N ewcarc(E, F, 'P) can be decomposed into a series of primitive N ewcarc opera­ tions each of whose added formula is just a single clause.

Proposition 2.8 Let F = C1 1\ · · · 1\ Cm be a CNF formula. Then,

Finally, the characteristic clauses Carc(E, 'P) can be expressed by constructively using primitive N ewcarc op­ erations. Notice that for any atomic formula p, if E ~ p, E ~ -.p, and p V -.p belongs to some stable production field 'P, then p V -.p belongs to Carc(E, 'P).

2.2 Applications

We illustrate how the use of the (new) characteristic clauses enables elegant definition and precise under­ standing of many AI problt-ms.

2.2.1 Propositional Case

In the propositional case, .A is reduced to the set of propositional symbols in the language. The subsumption relation is now very simple: a clause C subsumes D if C ~D. A theorem of E is called an implicate of E, and the prime implicates [Kean and Tsiknis, 1990] of E are:

The characteristic clauses of E with respect to 'P are the prime implicates of E belonging to 'P. When 'P = 'P c, it holds that Carc(E,'P) = PI(E) 3 .

Computin~ prime implicates is an essential task in the ATMS lde Kleer, 1986] and in its generalization called the clause management system (CMS) [Reiter and de Kleer, 1987]. The CMS is responsible for finding min­ imal supports for the queries:

Definition 2.10 [Reiter and de Kleer, 1987] Let E be a set of clauses and C a clause. A clause S is a support for C with respect to E if: (i) E I= SUC, and (ii) E ~ S. A support S for C with respect to E is minimal if no other support S' for C subsumes S. The set of minimal supports for C with respect to E is written M S(E, C).

The above definition can be easily extended to handle any formula instead of a clause as a query. Setting the production field to 'P c we see that:

Proposition 2.11 [Inoue, 1990] Let F be any formula.

When we choose the primitive N ewcarc operation as a basic computational task, the above proposition does not require computation of PI(E). On the other hand, the compiled approach [Reiter and de Kleer, 1987] takes P I(E) as input to find M S(E, C) for any clause C easily:

In the ATMS (de Kleer, 1986], there is a distin­ guished set of assumptions A ~ C. An ATMS can be defined as a system responsible for finding the nega­ tions of all minimal sup.E_orts for the queries consist­ ing of only literals from A [Reiter and de Kleer, 1987; Inoue, 1990]. Therefore, the ATMS label of a formula F relative to a given theory E and A is characterized as

Inoue [1990] gives various sound and complete methods for both generating and updating the labels of queries relative to a non-Horn theory and literal assumptions.

2.2.2 Abductive and Nonmonotonic Reasoning

The task of the CMS/ ATMS can be viewed as propo­ sitional abduction [Reiter and de Kleer, 1987; Levesque, 1989; Inoue, 1990]. For general cases, there are many proposals for a logical account of abduction [Pople, 1973; Cox and Pietrzykowski, 1986; Finger, 1987; Poole, 1989; Stickel, 1990], whose task is defined as generation of ex­ planations of a query.

3 The prime implicant· of a disjunctive normal form for­ mula can be defined in the same manner if the duality of A and V is taken into account.

Definition 2.12 Let :E be a theory, H ~ .C (called the hypotheses), and G a closed formula. A conjunction E of ground instances of H is an explanation of G from (:E, H)

if: (i) :E U {E} f= G and (ii) E U {E} is satisfiable 4 ·

An explanation E of G is minimal if no proper sub­ conjunction E' of E satisfies :E U {E'} F= G.

An extension of (:E, H) is the set of logical consequences ofTU{M} where M is a maximal conjunction of ground instances of H such that T U { M} is satisfiable.

Abduction can be characterized as follows:

Proposition 2.13 [Inoue and Helft, 1990] The set of all minimal explanations of G from (:E, H) is

There is an extension of (:E, H) in which G holds iff

Another important problem is to predict formulas that hold in all extensions. This problem is known to be equivalent to circumscription under the unique-names and domain-closure assumptions. Proving a formula holds in a circumscriptive theory [Przymusinski, 1989; Ginsberg, 1989], as well as other proof methods for non­ monotonic reasoning formalisms (including explanation­ based argument systems [Poole, 1989] and variations of closed-world assumptions [Bossu and Siegel, 1985; Minker and Rajasekar, 1990]), are based on finding ex­ planations of the query, and showing that these expla­ nations cannot be refuted:

Proposition 2.14 [Inoue and Helft, 1990] Suppose that Lp = p+ U Q+ U Q-, where P is the minimized predicates and Q is the fixed predicates in circumscrip­ tion policy and that P = ( Lp } . Every circumscriptive minimal model satisfies a formula F if and only if there is a conjunction G of clauses from Thp (:E U { ...,p}) such that N ewcarc(:E, ...,a, P) = 0.

Since we have characterized the prime implicates, the CMS/ ATMS, abduction and circumscription 5 , any ap­ plication area of these techniques can be directly char­ acterized by using the notion of the (new) characteristic clauses: for instance, diagnosis, synthesis [Finger, 1987] (plan recognition, prediction, desi~n), and natural lan­ guage understanding [Stickel, 1990J.

3 Ordered-Linear Resolution for Consequence-Finding

We now present the basic procedure for implementing the primitive N ewcarc operation. The important fea­ ture of the procedure is that it is direct, namely it is both sensitive to the given added clause to the theory and restricted to searching only characteristic clauses.

'This definition is based on [Poole, 1989] and deals with ground explanations. To get universally quantified explana­ tions, we need to apply the rever&e Skolemization algorithm [Cox and Pietrzykowski, 1986].

5 When a query in abduction or circumscription contains existentially quantified variables, it is sometimes desirable to know for what values of these variables the query holds. This an&wer extraction problem is considered in [Helft et al., 1991].

3.1 Basic Procedure

Given a theory E, a stable production field P and a clause C, we show how N ewcarc(:E, C, P) can be com­ puted by extending C-ordered linear resolution 6 . As seen in Propositions 2.8 and 2.9, both N ewcarc(E, F, P) for a CNF-formula F and Carc(E, P) can be computed by using this primitive N ewcarc operation. There are two reasons why C-ordered linear resolution is useful for computing the new characteristic clauses:

1. A newly added single clause C can be treated as the top clause of a linear deduction. This is a desir­ able feature for consequence-finding since the pro­ cedure can directly derive the theorems relevant to the added information.
2. It is easy to achieve the requirement that the pro­ cedure should focus on producing only those the­ orems that belong to P. This is implemented by allowing the procedure to skip the selected literals belonging toP. The computational superiority of the proposed technique compared to set-of-support resolution that is used by Finger's resolution residue [Finger, 1987], apart from the fact that C-ordered linear resolution contains more restriction strategies in natural ways, comes from this relevancy notion of directing search to P.

Some procedures are known to perform this computa­ tion for restricted theories 7 . For propositional theories, Siegel [1987] proposes a complete algorithm by extending SL-resolution [Kowalski and Kuhner, 1971]. Inoue and Helft [1990] point out that MILO-resolution [Przymusin­ ski, 1989], an extension of OL-resolution [Chang and Lee, 1973], can be viewed as C-ordered linear resolution with skip operation for ground theories with a particular pro­ duction field for circumscription (see Proposition 2.14).

The following proposed procedure called SOL {Skip­ ping Ordered Linear) resolution is a kind of generaliza­ tion of [Przymusinski, 1989; Siegel, 1987]. An ordered clause is a sequence of literals l?ossibly containing framed literals [Chang and Lee, 1973J which represents literals that have been resolved upon: from a clause C an or­ dered clause C is obtained just by ordering the elements of C; conversely, from an ordered clause C a clause Cis obtained by removing the framed literals and converting the remainder to the set. A structured clause ( P, Q} is a pair of a clause P and an ordered clause Q, whose clausal meaning is P U Q.

6 By the term C-ordered linear resolution, we mean the family of linear resolution using ordered clauses and the in­ formation of literals resolved upon. Examples of C-ordered linear resolution are Model Elimination LLoveland, 1978], m.c.l. resolution [Reiter, 1971], SL-resolution [Kowalski and Kuhner, 1971], 01-resolution [Chang and Lee, 1973], and the GC procedure [Shostak, 1976]. This family is one of the most familiar and efficient classes of resolution for non-Horn theories because it contains several restriction strategies.

7 Bossu and Siegel's [1985] saturation procedure finds Carc(E, P) where Lp are fixed to ground atoms. However, it does not use C-ordering, but A-ordering (a total ordering of all the ground atomic formulas).

Definition 3.1 Given a theory E, a clause C, and a production field P, an SOL-deduction of a clauseS from E + C and P consists of a sequence of structured clauses Do, D1, ... , Dn, such that:

1. Do = ( 0, C).
2. Dn=(S, Cl).
3. For each D1 = ( Ps, Q,), P, U Qs is not a tautology.
4. For each D, = ( P,, Qs ) , P, U Q, is not subsumed by any Pj U Qi, where Dj = ( Pj, Qj) is a previous structured clause, j < i. This rule is not applied if D, is generated from D,_1 by applying 5(a)i.
5. Di+l = ( Pi+1 , Q,~1 ) is generated from D, = (Pi, Q, ) according to the following steps:
6. (a) Let I be the left-most literal of Q,. Pi+1 and Rs~1 are obtained by applying either of the rules:
7. (Skip) If P, U { /} belongs to P, then Pi+l = P, U { /} and .Rs~ 1 is the ordered clause ob­ tained by removing I from Qi .
8. (Resolve) If there is a clause B, in E such that -,k E B, and I and k are unifiable with mgu e, then pi+l = 1{0 and Rs~l is an or­ dered clause obtained by concatenating B,O and Q,O, framing 10, and removing -,kO.
9. (Reduce) If either
10. Ps or Q, contains an unframed literal k different from I (factoring), or
11. Q, contains a framed literall-,k l ( ancestry),

and I and k are unifiable with mgu 0, then Pi+l = P,O and .Rs~1 is obtained from Q,O by deleting 10.

• (b) Qi~l is obtained from Rs~1 by deleting every framed literal not preceded by an unframed lit­ eral in the remainder (truncation).

Remarks. (1) At Rule 5a, we can choose the se­ lected literal I with more liberty like SL-resolution or SLI-resolution [Minker and Rajasekar, 1990].

1. Rule 4 is included for efficiency. This is overlooked in OL-deduction (and so is in MILO-resolution), but is present in Model Elimination [Loveland, 1978].
2. When Pis in the form of ( Lp ), factoring (5(a)iiiA) can be omitted in intermediate deduction steps like Weak Model Elimination [Loveland, 1978]. In this case, Rules 3 and 4 are omitted, and factoring is performed at the final step, namely it is taken into account only for P, in a structured clause of the form ( P,, Cl ) .
3. ( 4) The selection of rules 5( a)i, 5( a)ii and 5( a)iii must be non-deterministic; for I E Lp any rule may be ap­ plied. This is not a straightforward generalization of MILO-resolution or Siegel's algorithm, because they do not deal with Reduce as an alternative choice of other two rules, but make Q,~1 as the reduced ordered clause of the ordered factor of .Rs~ 1 that is obtained by Skip or Resolve. Both Przymusinski and Siegel claim that the

lifting lemma should work for their procedures. Unfortu­ nately, this simpler treatment violates the completeness described below. Furthermore, even for proof-finding, 01-resolution, which also handles the ancestry rule as a subsequent rule of Resolve, is incomplete. For example, when the theory is given as ·

it is easy to see that E I= p( a). OL-refutation from E + ...,p(a): However, there is no

1. -,p(a)
2. p(x) V -,q(x) V -,p(a)

Here, each underlined literal denotes a selected literal in the next step. The clause (6) is the dead-end of the OL-deduction. Hence, the reduction rule must be an alternative rule. Model Elimination and SL-resolution deal with the reduction rule as an alternative.

The Skip rule (5(a)i) reflects the following operational interpretation of a stable production field P: by Defini­ tion 2.1 (4), if a clause C does not belong to P and a clause Dis subsumed by C, then D does not belong toP either. That is why we can prune a deduction sequence if no rule can be applied for a structured clause D,; if Skip was applied nevertheless, any resultant sequence would not succeed, thus making unnecessary computation.

Theorem 3.2 (Soundness and Completeness) (1) If a clause S is derived using an SOL-deduction from E + C and P, then S belongs to Thp(E U {C}). (2) If a clause T does not belong to Thp(E), but belongs to Thp(E U {C}), then there is an SOL-deduction of a clauseS from E + C and P such that S subsumes T.

Recall that C-ordered linear resolution is refutation­ complete as shown, for example, by [Loveland, 1978], but is incomplete for consequence-finding [Minicozzi and Re­ iter, 1972]. Theorem 3.2 (2) says that SOL-resolution is complete for characteristic-clause-finding, and thus com­ plete for consequence-finding when P is P c.

Example 3.3 Consider the theory E and the clause C:

There is no OL-deduction of -,c from E + C, but -,c is derived using an SOL-deduction from E + C and P c as:

1. ( 0 , !! V b~ given top clause
2. ( 0, -,c V a V b) , resolution with (1)
3. ( -,c' en v Q ' skip and truncation
4. ( -,c, ~ V b ) , resolution with (2)

(7) ( -,c , [11 ) .

factoring and truncation

Note that an OL-deduction stops at (4).

Definition 3.4 Let Ll(E, C, P) be the set of clauses de­ rived using all SOL-deductions from E + C and P. The production from E + C and Pis:

Theorem 3.5 Let C be a clause.

Theorem 3.5 says the primitive N ewcarc(E, C, P) is contained in the production from E + C and P. To re­ move the clauses in the production derivable from E, we can use proof-finding: E f= S iff there is an SOL­ deduction of D from E + ..,s and { 0}. However, when the characteristic literals Lp is small compared with the whole literals £, the computation of Carc(E, P) can be performed better as the search focuses on P. Then, the check can be reduced to subsumption tests on Carc(E, P) by Proposition 2.5. The role of Carc(E, P) in this case is similar to the minimal nogoods in the ATMS [de Kleer, 1986]. This checking can be embed­ ded into an SOL-deduction by adding the following rule:

Proposition 3.6 If Rule 4a is incorporated into SOL­ deduction, then Prod(E, C, P) = N ewcarc(E, C, P).

3.2 Computing Prime Implicates

If the given theory is propositional, the prime implicates can be constructed using every clause as a top clause:

Proposition 3. 7 [Inoue, 1990] Given P /(E) and a clause C, P I(E U { C}) can be found incrementally:

Notice that, in practice, no tautology will take part in any deduction; tautologies decrease monotonically. The computation of all prime implicates of E by Proposi­ tion 3.7 is much more efficient than the brute-force way of resolution proposed in [Reiter and de Kleer, 1987]. Also, ours uses C-ordered linear resolution and thus nat­ urally has more restriction strategies than set-of-support resolution that is used in Kean and Tsiknis's [1990] ex­ tension of the consensus method.

This difference becomes larger when there are some distinguished literals representing assumptions in ATMS cases. The most important difference lies in the fact that the formulations by [Reiter and de Kleer, 1987; Kean and Tsiknis, 1990] require the computation of all prime implicates whereas ours only needs characteristic clauses that are a subset of the prime implicates [Inoue, 1990].

4 Variations

In Step 5a of an SOL-deduction (Definition 3.1), we treat two rules Skip (Rule 5(a)i) and Resolve (Rule 5(a)ii) as alternatives in order to guarantee the completeness of SOL-resolution. In this section, we violate this require­ ment, and show efficient variations of SOL-resolution and their applications to AI problems. Note that Re­ duce (Rule 5(a)iii) still remains as an alternative choice of other two rules (see Remark (3) of Definition 3.1).

4.1 Preferring Resolution

The first variation, called SOL-R deduction, makes Re­ solve precede Skip, namely Skip is tried to be applied only when Resolve cannot be applied. In a special case of SOL-R deductions, where the production field is fixed to P.c, Skip is always applied whenever Re­ solve cannot be applied for any selected literal in a de­ duction. In abduction, the resultant procedure in this case "hypothesizes whatever cannot be proven". This is also called dead-end abduction, which is first proposed by Pople [1973] in his abductive procedure based on SL­ resolution [Kowalski and Kuhner, 1971] 8 . The criterion is also used by Cox and Pietrzykowski [1986].

4.2 Preferring Skip

The next variation, called SOL-S deduction, places Skip and Resolve in the reverse order of SOL-R deductions. That is, when the selected literal belongs to Lp, only Skip is applied by ignoring the possibility of Resolve.

This skip-preference has the following nice properties. Firstly, this enables the procedure to prune the branch of the search tree that would have resulted from the lit­ eral being resolved upon. Secondly, SOL-S deductions are correct model-theoretically. Let us divide the set of clauses A produced by using SOL-deductions from E+C and P into two sets, say A1 and A2, such that

Note that Prod(E, C, P) = JJA. Then adding A2 to A1 does not change the models of E U A1 :

where M od(T) is the models ofT. Thus only A1 needs to be computed model-theoretically. The next theorem shows SOL-S deductions produce precisely such a A1 .

Theorem 4.1 If a clause T is derived by an SOL­ deduction from E + C and P, then there is an SOL-S deduction of a clause S from E + C and P such that EU{S} f= T .

In abduction, recall that for a clause S E A and H = Lp, ..,sis an explanation of ...,c from (E, H) if E ~ S. Thus, an explanation in A1 is the weakest in the sense that for any clause S2 E A2, there exists a clause S1 E A1 such that E u { -,S2} != -,S1 holds 9 ·

In circumscription, this is particularly desirable since we want to answer whether a query holds in every min­ imal model or not; the purpose of using explanation­ based procedures is purely model-theoretic. One of ad­ vantages of Przymusinski's [1989] procedure lies in the fact that MILO-resolution performs a kind of SOL-S de­ ductions [Inoue and Helft, 1990].

4.3 Between Skipping and Resolving

One further generalization of this kind of yreference would lead us to best-first abduction. Stickel L1990] uses the minimal-cost proof where we can choose each oper­ ation whose expected computational cost is minimum, but it is difficult to apply the idea to non-Horn theories.

8 Pople's synthesi1 operation performs "factor-and-skip". 9 An explanation E1 is said to be less-presumptiiJe than E2 if E U { ~} F E1 [Poole, 198 9]. Therefore, an explanation in A1 is a least-presumptive explanation of ...,c from (E, H).

5 Conclusion

We have revealed the importance of consequence-finding in AI techniques. Most advanced reasoning mechanisms such as abduction and default reasoning require global search in their proof procedures. This global character is strongly dependent on consequence-finding, in particu­ lar those theorems of the theory belonging to production fields . That is why we need some complete procedure for consequence-finding. For this purpose, we have proposed SOL-resolution, an extension of C-ordered linear resolu­ tion augmented by the skip rule. The procedure is sound and complete for finding the (new) characteristic clauses. The significant innovation of the results presented is that the procedure is direct relative to the given production field. We have also presented incomplete, but efficient variations of the basic procedures with nice properties.

Acknowledgment

I especially wish to thank Mark Stickel for his valuable comments on SOL-resolution and Nicolas Helft for dis­ cussion on earlier work. I would also like to thank Ray Reiter, Ryuzo Hasegawa, Koichi Furukawa and Wolfgang Bibel for helpful suggestions on this topic, and Kazuhiro Fuchi for giving me the opportunity to do this work.