An Inference Rule for Hypothesis Generation

1 Introduction

Traditionally automated deduction systems are devoted to prove if a given formula is a theorem; their applica­ tions , as is well knwon, have been very succesful in many domains of Computer Science. Gradually this tradition­ al functionality has been extended.

For example in Logic Programming, or in Deductive Databases, it is not enough to know if a closed formula is a theorem, indeed we want to know the set of substi­ tutions used in the proof of a formula.

Recently applications, like ATMS, automated diagno­ sis, generation of "why not" explanations, conditional answering in Deductive Databases, partial deduction, all Luis Farinas del Cerro IRIT U niversite Paul Saba tier 118 route de Narbonne 31052 Toulouse, France of them involving some kind of abductive reasoning, have emphasized the need of new functionalities. For every of these new applications it is necessary to produce, for a given formula, the set of hypothesis we have to add to a given theory to prove this formula. This shows that we are now expecting from an automated deduction method more information than an answer of the form : "yes" , or "no", or a set of substitutions.

*This work has been partially supported by the CEC, in the context of the Basic Research Action, called MEDLAR.

For these new aplications (see [7, 9, 11, 1, 5], and Inoue [4] for hypothesis generation) the expected information is, for a given Database DB, and a given query Q which is not derivable from DB, the set of hypothesis X such that X - Q is derivable from DB, and X is as general as possible. Such X are called the minimal supports for Q by Reiter and de Kleer in [14].

In order to mechanize the production of hypothesis some new algorithms have been defined. For example, in the frame of Profositional Calculus, by Siegel [13], Cayrol and Tayrac 10], Oxusoff and Rauzy [12], and Kean and Tsiknis [6], and in the frame of First Order Calculus, by Cholvy [2], and Inoue [4].

The objective of this paper is to present a new infer­ ence rule, and its associated strategy, which have been designed in order to efficiently compute the minimal sup­ port for a query.

We shall assume the reader is familiar with traditional theorem proving techniques as they are presented in [3] .

2 General definition of the generation hypothesis problem

In all the paper we consider a First Order Language where formulas are in clausal form.

Let S be a set of consistent clauses, a query adressed to S is represented by a literal L.

It is not restrictive to have only query represented by a single literal. Indeed, if the query is a first order formula F we can introduce a new atomic formula Q, and we can add to S the clauses generated by the clausal form of : Q +-+ F. Then the answer to the query Q provides the minimal support for Q.

The answer to the query L, relative to S, is a set of clauses containing instances of L, defined by :

ans(L,S) = { L'VX I S 1- L'VX, where L' is an instance of L, and L' V X is not a tautology, and there is no clause c derivable from S such that c strictly subsumes L' V X 1 }

According to this definition the clauses in ans(L,S) are minimal with regard to the subsumption.

If L' V X is in ans(L,S), the negation of X is an hy­ pothesis which allows to infer L' in the context of S.

It is worth noting some consequences of the condition of minimality. If L' V X is minimal we have :

• L' is not derivable from S. That means that ifL'VX is in the answer, we need additional hypothesis to derive L'.
• X is not derivable from S. Therefore the correspond­ ing hypothesis to infer L' is consistent with S.
• there exists no clause L' V X' derivable from S such that L' V X' subsumes L' V X. Since the condition L' V X' subsumes L' V X implies X' subsumes X, there is no weaker hypothesis than X to infer L' in the context of S.

A consequence of L' V X not being a tautology is that X is not the trivial hypothesis ...,L'.

Example!:

Let L=P( a,x) be the query, the answer is :

3 Definition of the Inference Rule

Definition 1. Let L be a literal. A clause C is an L­ clause iff there is a literal L' in C such that L is an instance of L'.

1 We say that c "strictly subsumes" c' if c subsumes c' and c' does not subsumes c

Definition 2. Let L be a literal and let MiYei , 1 ~ i ~ p, be a set E of clauses, called electrons, such that each Mi is a literal, and each ei is an L-clause. Let n be the clause : N1 V N2 V ... V Np V n', where the Ni's are literals, which is called the nucleus. A finite sequence of L-clauses Ro, ... , Rp is an L-inference iff :

• Ro is n,
• each Ri+l is a resolvent obtained (by the Resolution principle) from Ri and MiVei, where the literal Mi is resolved against the instance of the literal Nj, which is in Ri, 1 ~ j ~ p.

Rp is called the L-resolvent of E and n, and the Ri, for 1 ~ i ~ p - 1, are called the intermediate resol­ E n vents. The L-inference will be represented by : -­ Rp

Definition 3. Let S be a set of clauses. A L­ deduction of Cn from S is a finite sequence Co ... Cn of clauses such that : each Ci is either a clause in S or there are Ch, ... Cik in the L-deduction, with each ij < i, such that ci is the L-resolvent of cil' ... cik' by an L­ inference whose nucleus is in S.

Definition 4. A R-deduction of Cn from S is a finite sequence Co .. . Cn of clauses such that : each Ci is either in S or there are Cit, Cb in the R-deduction, with each ij < i, such that ci is the resolvent ( by the Resolution Principle) of Ci 1 and Cil.

Theorem 1. (R.C.T. Lee [8]) Let S be a set of clauses, if c is a clause derivable from S, there is a clause c', subsuming c, such that c' is derivable from S by a R-deduction.

Theorem 2. Let S be a set of clauses and L a given literal. If there is a R-deduction of LV C, then there is a L-deduction of LV C.

Proof. The proof is by induction on the number n of inferences in the R-deduction of L V C from S.

For n=1, LV Cis the resolvent of two clauses C1 and C2 in S. Then either C1 or C2 ( say C1 ) is of the form M Ve, where e is a L-clause, and M is the resolved literal. Therefore the R-inference is a L-inference.

For the induction step we assume we have a R­ deduction of LV C from S using n inferences. Let's consider in this R-deduction some clause Co which is the resolvent of two clauses cl and c2 which are ins.

Then there is a R-deduction of L V C from S and Co using n-1 inferences.

We distinguish the following two cases:

Case 1. Co is a L-clause. For the same reason as in h b . d t' Ct C2 . L . r Th t e ase m uc 1on step Co 1s an -mterence. en by induction hypothesis the R-deduction of L V C from S and Co there exists a L-deduction D of L V C from S and C0 . If we add the L-inference : C 1 CoC 2 before the first occurence of Co in D, we get a L-deduction of LV C from S.

Case 2. C0 is not a L-clause. Then by induction hy­ pothesis there exists a L-deduction D of L V C from S and Co. Assume the L-inference using Co, in D, is of the form E c:o , where E is a set of electrons and Co is the nucleus .We define a partition of the set E into two sets E1 and E2 as follows : a clause e in E is in E1 if and only if the literal in e which is resolved in the inference E c:o is provided by the clause C1.

Then we transform the proof d : E~ Co c3 ~ where c3 c1 c2 is an L-inference, and Co 1s an

R-inference,

. E1 c1 d E2 c2 The mferences c 4 an Cs are Linferences, because E c:o is a L-inference, i.e. each intermediate resolvent in the L-inference is an L-clause, and the resolved literals in E1 (resp. E2) and Ct (re­ sp. C2) are the same literals as the literals resolved in E and Co. Then C4 and Cs are L-clauses, and in the . r C4 Cs h I d I' I h lDterence : c6 , t e reso ve ltera s are t e same

· h · r C 1 C2 th l't I as m t e mterence : Co ; moreover ese 1 era s are not the literals which make C4 and C5 be L-clauses, then C 4 c 6 Cs is an L-inference. So C6 is an L-clause, and the transformed proof d' is an L-deduction.

The set ofliterals which must be unified, and resolved, in the proof d and in the proof d' are the same, then the two sets of equations defining the most general unifiers in d and d' are the same. Then the substitution applied to the literals ofE, C1 and C2, whose instances are in C3, is the same as the substitution applied to the literals of E1, E2, Ct and C2 whose instances are in C6 . Therefore C6 is identical to C3. Finally if we replace in D the proof d by d' we get an L-deduction of LV C from S.

In the case where there are several occurences of Co in the proof D, and Co is involved in several L-inferences of E' C the form C' 0 , we remove each Co occurence with a 3

similar transformation. Notice that each transformation decreases by one the number of Co occurences. Then after a finite number oftranformation of the L-deduction D we obtain a L-deduction of LV C from S. Q.E.D.

The following completeness theorem is a trivial conse­ quence of Theorem 1 and Theorem 2.

Theorem 3. Let S be a set of clauses, if LV c is a clause derivable from S, there exists a clause L' V c', subsuming L V c, which is derivable from S by an L­ deduction.

Proposition Since every L-inference is a sequence of application of Resolution principle, the L-inference rule is sound.

One could notice that an L-deduction is very close to an OL-deduction, or an SL-deduction (see [8]) with top clause ...,L, However OL-resolution has been proved to be complete to generate the empty clause, but it fails to be complete for clause generation. Inoue, in [4], modi­ fied the standard OL-resohition, by adding a new rule, called "Skip", that allows to reach completeness. The complexity of the proof of Theorem 1 clearly suggests that there is no evidence that a strategy which is com­ plete to generate the empty clause is also complete for the generation of clauses. That is why the proof of The­ orems 2 and 3 is, in our view, the main contribution of our work.

4 Definition of the L-strategy

A saturation algorithm is considered in order to define an effective procedure to compute the L-clauses. This algorithm could be improved using more sofisticated s­ trategies like ordering.

The L-strategy computes the answer to a query into two steps. In the first step is computed a set of clauses, called extended answer, containing more clauses than the clauses in the answer. Namely answers may contain hypothesis which are inconsistent with S. In the second step we have to remove all the clauses L' V X in the extended answer such that X is derivable from S. In this second step the clause X is known, then testing if X is derivable from S can be done by any standard theorem proving strategy. For this reason this second step is not described in this paper, and we shall present only the first step.

Definition 5. We call extended answer the follow­ ing set of clauses :

eans(L,S) = {L'VX IS 1- L'VX, where L' is an instance of L, and L' V X is not a tautology, and there is no clause c in eans(L,S) such that c strictly subsumes L' V X }

Note that this definition is weaker than the previous one. Indeed, if L' V X E ans(L, S), X is not derivable from S, while if L' V X E eans(L, S), X may be derivable from S.

Notation : We denote [S] a set of clauses where all the subsumed clauses have been removed.

Definition 6. Let S be a set of clauses, and let L be a query, the L-strategy computes the sets S0 , ·.. , Si+l, ... , inductively as follows :

So = [ {(L' V X)u I L' V X E S and u is the most general unifier of L and L' } ]

si+l = [Si u {L' y X I there exists a set ~f ele~trons E in Si, and a nucleus n in S, such that L V X IS the L'-resolvent of E and n}]

For the purpose of the next definition we consider de­ ductions as proof-trees instead of proof-sequences.

Definition We call depth of a deduction the num­ berofinference steps in the longest path of the proof-tree corresponding to this deduction.

Theorem 4. If L' V X is in eans(L,S), where L' is an instance of L, then there exists some i, and a clause c, such that c is in Si, and cis equivalent to L' V X

Proof : The proof is by induction on the depth j of the L' -deduction of L' V X from S.

For the base case (j=O) the proof is trivial.

For the induction step, assume there is an L'­ deduction, of depth j + 1, of L' V X from S, where the last L'-inference is of the form ~~v~

First we show that tautologies can be removed.

If a L' V X proof uses a tautology, then we can show by induction that this tautology is either n or an electron of E. In that case we can also show that it is possible to transform the last two inferences in a proof whithout tautology.

Now we show that subsumed clauses can be removed.

Let e = M V e' be an electron in E, where M is the resolved literal. If e does not belong to eans(L,S), there is an L-clause c in eans(L,S) subsuming e. We distinguish the following two cases :

Case! : c susbsumes e'. Then c subsumes the instance of e' which is in L' V X. That contradicts the fact that L' V X is in eans(L,S).

Case2 : c does not subsumes e'. Then c is of the form M'Vc', where M' is an instance ofM. In this case we can . E n b l . . Eb transform the mference L'VX y rep acmg e m y c. Then the new L' -resolvent subsumes L' V X because c' subsumes e' . That contradicts the fact that L' V X is in eans(L,S).

Therefore e belongs to eans(L,S). Since the depth of the L'-deduction is equal to j, by induction hypothesise isinSj.

The same conclusion holds for any electron in E, so from the definition of Sj+l in function of Sj we can con­ clude that L' V X is in Sj+l·

5 Some typical examples

In this section we present two examples showing the main features of our approach.

Example2 is a very simple example illustrating the interest of the L-strategy for automated diagnosis.

Let's consider a very simple system l, with components : b, b1 , b2, and c, whose correct working is defined by the following rules and facts :

l - works +- b - works A c - works b - works +- b1 - works A b2 - works b1 - works

If we respectively denote by : L, B, B1, B2 and C, the propositions : !-works, b-works, b1 -works, b2-works and c-works, we have :

Query: L

The answer : L V -,B2 V ...,c can be interpreted as : "!-works if b2-works and c-works", or as well as : " a possible explanation that l does not work is that b2 or c does not work".

Example3, which is in Propositional Calculus, is in­ teresting because it shows that the standard Input reso­ lution strategy is not complete. Indeed with this strategy we cannot infer L VA, while L VA is derivable with the L-strategy. Here we can see that the reason why the L­ strategy is complete, although it is an Input strategy, is that the L-strategy is also an Hyperresolution.

S = { L V M V N, -.M V N, M V -.N, -.M V -.N VA }

Query: L.

So = {LVMVN}

S1 {LV M, LV N}

The clauses : LV NV -.NV A, and LV M V -.M VA are not in S1 because they are tautologies, and LV M V N is not in S1 because it is subsumed by LV M.

S2 = {L V M, L V N, L V A}

L V A is generated by an L-inference where the two electrons are : L V M and L V N, and the nucleus is : -.M V -.N V A. The clauses L V -.M V A and L V -.N V A are not in S2 because they are subsumed by L V A.

Example4 shows how we can get infinite answers. The intuitive meaning of the query is : What conditions implies that x is an ancestor of y ?". Since the query does not refer to a specific set of persons, there is an infinite set of conditions which guarantee that x is an ancestor of y; each condition correponds to a different level in the ancestor's hierarchy.

S = {L(x, y) V -.Ancestor(x, y), Ancestor(x, y) V -.Father(x, y), Ancestor(x, y) V -.Ancestor(x, z) V -.Father(z, y) }

Query : L(x,y).

So = {L(x, y) V -.Ancestor(x, y) }

Si = {L(x, y) V -.Ancestor(x, y), L(x, y) v -.Father(x, y), L(x, y) V -,Father(x, zl) V -.Father(z1, y), L(x, y) V -.Ancestor(x, z2) V -.Father(z2, zl) V -.Father(zl, y),

L(x,y) V -.Ancestor(x,zi) V -.Father(zi,Zi-d V . .. V -.Father(z2, zl) V -.Father(z1, y)}

6 Conclusion

We have defined an inference rule and a strategy to gen­ erate the most general hypothesis allowing to infer a for­ mula, represented by a single literal L, in the context of a given theory. This strategy is efficient in the sense that it generates only L-clauses. Then the only useless gen­ erated closes are those ones which are not minimal with regard to the subsumption. Moreover we have the feel­ ing that this second step cannot take advantage of the work done in the first step, and they can be executed into two independent steps without waste of efficiency.

Nevertheless many refinements of the strategy should be investigated in the future. One of them is to make use of an order on the predicate symbols.

An important issue we want to investigate in the fu­ ture is the case of infinite answers. A first approach is to find a finite representation of those infinite sets, having some desirable properties. For example to be easy to understand. Another approach is to provide only partial answers, and to cut the computation in a "clean" state. The right approach certainly depends on the application field.

Our method can be considered as a step in order to supply new functionalities for automated deduction methods.

Acknowledgements

Thanks to reviewers for their constructive and valuable comments.