A Model Elimination Calculus for Generalized Clauses

1 Introduction

Several extensions of the resolution rule and its refine­ ments have been propo11ed able to deal with quantifier free first order logic formulas (e.g. see (Murny, 1982] for an e.xtension of the resolution rule and [Stickel, 1982] for a modification of tlte connection-graph procedure). These proof procedures have the advantage that it is not necessary to build a dausalnormal from, i.e., despite from establishing a prenex normal form and skolemizing existentially qlllmtified variables no nonnalization oper­ ation!! are necesRary. Tltis enhances the readability and understandability of proofs and can also lead to shorter deduction11.

However, these modifications do not necessarily ex­ ploit the control structure implicit in logical formulas. In particular, although o.n implication a --+ b 1\ c is not broken into two clauses -,a V b and -,a V c, it is not ex­ cluded that a has to be proven twice in a proof of b 1\ c. This happens when, for instance the proof search per­ forlllf! a kind of backward chaining.

In this paper we pre11ent an extension of the xnodd elimination calculus [Loveland, 1969a, Loveland, 1978] which overcomes this drawback. It works on so called generalized clanu~ which arc disjunctions of complex lit­ eral8 being conjunctions of (simple) literals. For exam­ ple, the implication (a V b) --+ ( c 1\ d) is equivalent to the generalized clause (-,a 1\ ..,b) V ( c 1\ d) where -,a 1\ -,h and c 1\ d are complex literals.

This restriction to generalized clauses is mainly moti­ vated by pragmatic conRiderations, as we use the ex­ tended model elimination calculus for processing the predicate logic Eart of the knowledge representation lan­ guage LLILOG [Pletat and v. Luck, 1990, Bollinger and Pleta.t, 1991] in the LEU /2 1 text 1mderstanding and question answering syRtem [Geurts, 1990] . Items of a knowledge base need to be easily comprehensible. This is the case for Prolog like rules and facts, but not for arhitrary logical formulas. Even if they are quite simple they can hP- misinterpreted, e.g., for seeing that. the for­ mulae a--+ (b--+ c) and (a--+ b)--+ care not equivalent one needs at least some basic knowledge in logic. On the other hand by using definite or indefinite clauses, knowl­ edge cannot he expressed in a compact way. Generalized clauses arc therefore a good compromise. Rules with a conjuntive conclusion or a disjunctive premise are not torn apart . Equivalences between conjunctions of liter­ als can be represented by two generalized clauses.

In the next section we explain how Loveland's wcnk modd elimination calcuhtB can be adapted to generalized clmtBes. Compared to Loveland's calculus, deductions in this calculm1 require in general less inference steps as well as less computations. We then describe a method for generating lemmas. Using these lemmas, we show that. redundant proofs of the premises of rules with a con­ junctive conclusion can be avoided. We conclude with a discussion of the calculus.

2 Extending Model Elimination to Generalized Clauses

2.1 Model Elimination for Ordinary Clauses

Modd Eliminat.ion 2 can he considered as a refinement of linear resolution where resolution steps are restricted to input clauses. Resolution steps with predecessor clauses in the proof tree are simulated by the reduction rule. For this it. is necessary to mark resolved literals instead of deleting them.

1 LEU is the acronym for "LILOG Experimenticrnmge­ bung" - LILOG experimental environment.

2 To be more precise it is Loveland's weak model elimi­ nation method [Loveland, 1978] that we will present in the following.

More precisely, instead of clauses, we lmve chain8 which are ordered sequences of ordinary literals, called O-literal8, and resolved literals, R-literal8. R-literals are enclosed in brackets ([L]) for distinguishing them from 0-literals. Chains containing only 0-literals are elemen­ tary chains. Unit chains consist of only one literal. We call the universal closure of the disjunction of its 0literals the clatual interpretation of a chain. A chain is called admiuible if the rigbt-most literal is an 0-literal 3 · The contraction-operation transforms a chain into an ad­ missible one by removing all R-literals to the right of the right-most 0-literal.

The model elimination method consists of two infer­ ence operations:

• the exten.,ion rule corresponding to the resolution ntle and
• the redttdion rttle.

For defining them we use the notion of complementarity of literal8:

Definition 1 (Complementarity of literals) Two literal8 L1 and L2 can be made complementary with a mod general tmifier 0 iff L1 and the complement of L2 are unifiable 11.1ith a mo8t general unifier 0.

The two model elimination rules are defined as follows:

Definition 2 (ME extension) Let c1 = c~£1 and c2 = c~L2c~ be two admiuible chain8, LJ and L2 be O­ literal8 and a be a renaming of the t1ariable8 in c2 8uch that c1 and c2a hat1e no t1ariable8 in common. If L1 and L2a can be made complementary with a mod gen­ eral unifier 0, then the contraction of (c~[LI)c~ac~a)0 i8 called the ME extension of c1 111ith c2 ·

Definition a (ME reduction) Let c = c'[L1)c" £2 be an admi88ible chain. If L 1 and L 2 can be made com­ plementary with a mo~t general unifier 0 then the con­ traction of (c'[L1)c")0 i6 a re8ult of the ME reduction of c.

The rationale behind the reduction rule is that in a chain c'[L)c" the subchain c' L is always an instance of a c.hain used for an extension step. Hence the reduction of a chain corresponds to an extension step eventually followed by a factorization.

For completing the presentation of model elimination we have to introduce the notions of model elimination (ME) deduction and model elimination (ME) refutation:

Definition 4 (ME deduction) Given. a ,,ct S of ele­ mentary chain~, an ME deduction of a chain c from S i,, a finite uqtu:nce of chain8 c1 , ··. , c,. 111ith

• CJ E S,
• for i=f, ... ,n c; ;_,obtained by ME exte1Mion of Ci-1 with an ( attxiliary) chain. from S or by ME reduction ofci-1.
• c = c,..

1 Loveland's definition in [Loveland, 1978] contains 3 sup­ plementary conditions for the 'admissibility of chains. But it is easy to see and has already been stated in [Casanova et al., 1989] that their removal neither affects soundness nor completeness of (weak) model elimination.

Definition 5 (ME refutation) A reftttation of a 8et S of elementary chain6 i6 a deduction from S of the empty chain D.

Example 1 We will U6e the follou,ing example through­ ottt thi8 paper for illu6trating ottr modification_, of the dandard model elimination calcultu.

Gi'l!en the following axiom6:

ax1 : VxG(x) V Y(x)--+ C(x) A S(x),

ax2 : G(p) V Y(p),

111here G(x} may 6tand for "x i8 a gourmet", Y(x} for ''x i8 a yttppy", C(x) for "x like8 to drink champaign", S(x) for "x like8 to eat mail6" and p can be interpreted a8 "Peter", one like6 to prot1e the goal

g: 3xC(x) A S(x).

After having built a cla1ual normal form of the axiom8 and the negated goal we get the following refrttation of the re6ttlting 6et of chain8:

Extension and reduction are sound inference rules. Further they form .a (refutationally) complete calculus. The following two theorems state this in a more formal way:

Theorem 1 (Sound~ess of ME) If a chain c i ., the re61tlt of an. ME deduction frorn a 6et S of elernenta1·y chains, then the clatt~al interpretation of c is a logical conuquence frorn S.

Theorem 2 (Completeness of ME) If a set S of el­ ementary ch.ain8 i~ minimally tm6ati~fiable, i.e., if et1ery proper ntb8et of S is satisfiable, then for any chain c E S there i.e a ME refrttation of S 8tarting 111ith c.

2.2 Resolution for Generalized Clauses

First we formally define the notion of complex literal and geueralizcrl clause.

Definition 6 (Complex literal) A complex literal i6 a conjunction of (simple) literal~ .

Definition 7 (Generalized clause)

A generalized clattu is a disjunction of complex liter­ ak

When resolving two arbitrlny quantifier free formu­ las (see [Muray, 1982)) first the polarities of all atomic subformulas have to be determined. H they contain two unifiable atomic subformulas with opposite polar­ ity, the unifying substitution is applied to the two for­ mulas. Then all occurences of the atom with positive polarity are replaced by F, representing fal8e, and all oc­ currences of the negative atom in the other formula by T, standing for true. The disjunction of these two mod­ ified formul88 represents the resolvent, which is further simplified by exploiting properties of logical connectives like a 1\ F +-+ F or a V F +-+ a.

Adapting this resolution rule to generalized clauses is straightforward. In generalized clauses the sign of the simple litersls indicates the polarity of their atomic for­ mul88. During the resolution operation the positive lit­ eral is replaced by F, such that the complex litera~ it appears in can be reduced to F (complex literals are con­ junctions). Hence they can be removed from the resol­ vent. The same happens with the complex literals where the negative (simple) literal occurrs in, 88 its atomic for­ mula is replaced by T which is equivalent to replacing the literal by F. Therefore resolving two generalized clauses C01 and C02 consists of unifying a simple literal L1 of Co1 with the complement of a simple literal Lz from C02 , applying the unifying substitution 0 to Co1 V Coz and discarding from the resulting generalized clause all complex literals with occurrences of £ 10 or £ 20.

2.1 Model Elimination for Generalized Clauses

The notions introduced in Section 2.1 can e88ily be adapted to generalized clauses. Now we have com­ ple:r: 0- and R-literal8 and generalized chain8 consist­ ing of complex 0- and R-literals. Complex literals are noted 88 conjunctions of simple literals. If a com­ plex 0-literal consists of more than one simple literal it is enclosed in (round) parentheses. As before, R­ literals are marked by (square) brackets. The chain P(a)(Q(b)](P(b) 1\ R(a)](Q(c) 1\ P(c)), for instance, con­ sists of two complex 0- and R-literals.

The definition of admissibility and the contraction op­ eration have to be modified accordingly.

When resolving two generalized clauses only simple litersls are compared. This also holds when two com­ plex litersls are made complementary. We can therefore define the complementarity of complex literal8 in the fol­ lowing way:

Definition 8 (Complementarity of compl. literals) Let C1 = Lu 1\ .·· 1\ L1m and Cz = Lz1 1\ ·· · 1\ Lz,. be two comple:r: literal8. C1 and C2 can be made complemen­ tary, with a most general unifier 0, iff a 6imple literal Lli from C1 and the complement of a 8imple literal Lzj from Cz are nnifiable with mo8t general nnifier 0.

There may he more than one p011sible most general unifier for making two complex literals complementary; e.g. for P(a)AP(b) and -,P(:z:) we have two most general unifiers: 0 1 = {a/:z:} and 0 2 = {b/:z:}. But all the most general unifiers can be computed since the number of all simple literal pairs from two complex literals is finite.

When resolving two generalized clauses, all complex literals containing the resolved simple literals are dis­ carded. Deleting or bracketing these literals during an extension step may lead to complications, for complex literals standing left 'Of an R-literal may be deleted or transformed to ·an R-literal. It is therefore possible that the left suhchain relative to an R-literal is no longer an instance of a predecessor chain in a deduction. But this is a condition for the correctness of the reduction nue.

Fortunately, it suffices to bracket resp. delete oruy the complex literals that are made complementary. We can therefore define generalized model elimination (MGE} e:r:ten8ion and reduction rule in the following way:

Definition 9 (GME extension) Let C1 = qc. and C2 = C~C2C~' be two admiuible generalized chain6, C1 and C2 be complex O-literal8 and a be a renaming of the variable8 in C2 8uch that C1 and Cza hat~e no tlariable8 in common. If C1 and C2a can be made complementary with a mo8t general unifier 0, then the contraction of (C~[C 1 ]C~aC~a)0 i8 called the GME extension ofC1 with Cz.

Definition 10 (GME reduction) Let C = C'[C1]C" C2 be an admiuible generalized chain. If the complex literal6 C1 and Cz can be made complemen­ tary with a mo8t general unifier 0 then the contraction of (C'[C1]C")0 i8 a re1ult of the GME reduction of C.

GME deduction and GME refutation can be defined analogously to ME deduction and ME refutation. One has only to replace in Definition 4 and 5 "chain" by "gen­ eralized chain" and "ME" by "GME".

GME extension and GME reduction are sotmd infer­ ence rules. The soundness of GME extension follows from the soundness of resolution for quantifier free for­ nmlas. A GME reduction can be simulated by an exten­ sion 11tep with a predecessor clause in the deduction such tlu\t the clausal interpretations of the resulting cllains are equivAlent. Hence the GME reduction rule is sound too.

We get therefore the following theorem that can be proven by induction on the length of the concerning de­ duction:

TheoremS (Soundness of GME) If a generalized chain. C i_, the re8ult of a GME deduction from a .,ee S of elementary generalized chainll, then the clatt8al in­ terpretation of C i6 a logical con6equence of S.

The proof of the completeness of generalized model elimination is b88ed on the following lemma, where the function coc produces a kind of conjunctive normal forn1 of a generalized chain.

Lemma 1 Let S be a 6et of generalized elementary chain6 and let coc (''contained ordinary chain6 ") be a mapping from generalized chain6 to 6et6 of ordinary chain6 that i6 defined a6 follow6:

coc(C) = {LH 1 L2;, ... L,.;.II i; = 1, .. . ,mi,i = 1, ... ,n} 'IDith C = CtC2···C,., where Cj = Ljl 1\ ··· 1\ Ljm . i6 ei­ ther a complex 0- or an R-literal and Lj; in.herlte6 the literal type /rom Cj. Furthermore let S = Uces coc(C). If there i6 a ME-deduction of a chain c from S then there i6 al6o a GME-deduction of a generalized chain C from S 'IDith c E coc(C).

Given an ME-deduction of a chain c from S, the proof of this lemma consists essentially of constructing from S an isomorphic GME-deduction of a generalized chain C containing c. Being technical it is omitted here and can be found in an extended version of this paper [Bollinger, 1991].

Theorem 4 (Completeness of GME) If a 6d S of generalized elementary chain6 i6 minimally tm6ati6fiable, i.e., if et1ery proper 6ttb6et of S i6 6ati6fiable, then for any chain C E S there i6 a reflttation of S 6tarting with C.

Proof: A6 S i6 un6ati11jiable, S = Uces coc(C) i6 tm6ati6jiable too. Let S' ~ S be a minimally ttn6ati6fiable nsb6et of S. For any C E S we hat1e coc(C) n S' f. 0. If that would not be the cau, S\{C} would be un6ati6fiable {due to coc( S\ { C}) 2 S' ), 'IDhich contradid11 the auump­ tion that S i6 minimally un6ati6fiable.

Let c E coc(C) n S'. Due to the completen.e66 of model elimination there i6 a ME deduction of 0 11tarting with c. A6 c E coc(C) Lemma 1 can be applied and we obtain that there i6 al6o a GME deduction of 0 from S 11tarting 'IDith c. 0

3 Generating Lemmas

Although GME-refutations in general are shorter than the corresponding ME-refutations, we still have the problem of redundant proofs of premises, whose rules have conjunctive conclusions. In Example 2 we saw that the chain a1 was applied twice, whereas one applica­ tion should suffice. In chain (2) the "premise" literal -,G(x) 1\ ...,Y(x) of a1 stands to the right of the resolved literal. H this literal is proven one can deduce the con­ clusion. This is done by the two subsequent inference steps, i.e. at that moment C(p) 1\ S(p) should have been deduced M a lemma. How can we achieve this?

We introduce a third type of literals called lemma can­ didatell or L-literal11. When extending a chain C with an auxiliary t'hain Ca the resolved literal in Ca iR declnred M a lemma candidate and is put beside the brncketed lit­ eral, the resolved (complex) literal of C in the resulting chain. Lemma candidates are put into braces, such that in Example 2 above, the extension step of chain (1) with chain a1 yields:

(2') -,C(z)[...,S(z)]{C(z)/1. S(z)}(...,G(z) 1\ -,Y(z))

H it is possible to deduce the empty chain from the subchain to the right of an L-literal, the corresponding instantiation of the L-literal becomes a valid lemma.

More formally we have:

H C! f. 0 or C! f. 0, an extension step of C1 = Cf C1 with Ca = C!C2C; yields, c2 = (cf[.c.]{.c2}c!c;)0.

H there is a deduction of 0 starting with (C!C;)0 and if \1 is the composition of the most general unifiers in that deduction, then we also have a deduction of C20\J starting with (.C2C!C!)0.

The refutation of (C!C;)0 has to be performed when trying to refute C2 · Since rhains represent disjunctions of literals, it cannot be taken for granted that a refu­ tation of C2 contains also a refutation of (C~C!)0. For tltiR no literal of Cf [Ct] has to be involved in any ex­ tension or reduction step when, during the refutation of C2 , (C!C;)0 is processed. This is certainly the case if the literals in (C!C;)0 are elimiuated by exteusion steps. The situation is different for reduction steps . A reduc­ tion performed with an R-literal from Cf [C1] during the refutation of c2 can't be transferred to a refutation of ( C!C~ )0. For that the R-literal has to stand to the right of [C1J in C2 or a chain deduced from C2 .

We take into account this restrict.iou in the following way: Let us suppose that a reduction step can be applied to C = C 1 [.C2)C 2 C1 by makiug complementary the literals C1 and C2 . The lemma candidates in C 1 are not affected by this as the involved 0- and R-literal are on the right of C 1 · However, for the lemma candidates in C 2 the R­ literal [C2] stands to the left. Therefore these lemma candidatefl become invalid and have to be eliminated.

The modifications of the contraction operation, of the GME extension and the GME reduction rule are clear now. The contraction operation also deletes rightmost L-literals, that become valid lemmas. The extension rule may introduce a new L.literal being the "resolved" literal of the auxiliary chain. L-literals standing between the R- and 0-lite.ral involved in a reduction operation are deleted.

Example a The refutation of Example 2 i8 modified a11 fnllow8 if lemma8 are generated:

(a1 } (...,G(x) 1\ ...,y(z))(C(x) II S(z)) (a2) G(p)Y(p) negated goal: {1} ·C(z)...,S(x) exte1uion with (a1}: (2} -,C(:z:)[-,S(z)]{C(z) A S(z)}(...,G(z) 1\ -,Y(x)) exten8ion with (a2): (3} ...,c(p)[...,S(p)]{C(p) 1\ S(p)}[...,G(p) 1\ ·Y(p))G(p) red1tr.tion and generation of lemma (1) C(p) 1\ S(p): (4) ...,c(p) cxtcn~ion with (1) : {5} 0

Lovclaud also proposes a method for generating lcm­ Illt\.'1. ht [Loveland, 1969b], he introduceR the notion of unpe aRsodnt.ed with R-literals. It is initialized to 0 and updated when the R-literal is involved in a reduction step. ht that case, it is set to the maximum of its actual scope and the number of R-literals standing to the right. of it . H due to subsequent reduction and exteusion steps the scope exceeds the number N of R-literals to the right it i11 set to N. The subchain in the scope of an B.-literal LR with scope N is the subchain from LR to the N-th R-literal to the right.

Lemmas can be formed when an R-literal LR is re­ moved by the contraction operation. The maximal subchain in the scope of au B.-literal is taken iu which LR occurs (as the last literal). The lemma is generated by leaving the 0-literals unchanged and turning the nega­ tion of the R-literals into 0-literals.

Example 4 We 8how a part of a deduction where lem­ ma8 are generated. The indice8 of the R-literal8 indicate their uope.

(i) P(a)[Q(:z:))o[P(y)Jo-.Q(a)[R(z )Jo-.P(a) reduction without contraction: (i+1) P(a)[Q(x))o[P(a)h -.Q(a)[R(z)]o contraction and gen. of lemma -.P(a)-.Q(a)-.R(z): (i+1'} P(a)[Q(x)Jo[P(a)]t-.Q(a) reduction without contraction: (i+f} P(a)[Q(a)Jt[P(a)Jo contraction and generation of lemma -.Q(a)-.P(a): (i+t') P(a)

Specializing our method for lemma generation to or­ dinary chains we see that it corresponds exactly to the case where Loveland's method is restricted to the gen­ eration of unit lemma. chains. Lemma candidates are not explicitely recorded since for simple literals they are identical to the negation of the corresponding R-literal. For complex literals this is necessary, as we do not have .Ct0 = -.£2 0 in general when they are complementary.

The removal of lemma candidates after a. reduction step has its counterpart in the fact that, according to Loveland's method, the generation of lemmas is based on the maximal subchain in the scope of an R-literal yielding up to the rightmost R-literal. This has the effect that lemmas for R-literals within this subcha.in (except the leftmost one) are not created.

It is easy to generalize Loveland's method to general­ ized chains. In this way it is possible to generate lemmas being the instance of disjunctive conclusions. However, from a practical point of view, non-unit lemmas are less useful in general.

4 Discussion

Generalized clauses and chains are interesting extensions of their standard versions. Any quantifier free logical formula can be represented by one such clause or chain. This facilitates especially the processing of disjunctive goals. In contrast to ordinary chains (and clauses) a negated goal can always be transformed to exactly one generalized chain. Moreover, having a. set of ordinary chains representing the negated goal, a. refutation may succeed with only one of them as the starting chain. Hence for ordinary chains we have the problem of choos­ ing the right chain steming from the negated goal. This problem does not occur for generalized chainR, !Lt! we have only one goal chain, and from Lemma 1 we know, that its refutation succeeds if it succeeds for one of the ordinary goal chains.

From an implementational viewpoint, generalized model elimination (GME) constitutes only a slight mod­ ification of the model elimination method (ME). In con­ trast to resolution for arbitrary quantifier free formulas, not a lot of supplementary computation has to be per­ formed. The polarity of the literals has already been determined, only simple literals are compared when two complex literals are made complementary. The only real difference to ME consists in the fact that several sitn­ ple literals are deleted or bracketed during an extension and reduction operation. Of course, if lemmas should be generated, additional computations have to be per­ formed concerning the L-literals. But compared with Loveland's method for lemma generation their complex­ ity is not higher. The computational overhead of GME with respect to ME is therefore low.

However, as GME refutations are generally shorter than ME refutations, ( cf. Example 1 compared to Ex­ ample 2) the overall amount for computing a refutation is lower for GME. This effect is enhanced if lemmas are generated, since the really interesting lemmas are those generated for rules with co11junctive conclusions.

Looking at the search space, one realizes that the num­ ber of potential extension and reduction steps is greater for GME than for ME, since complex literals may consist of several simple literals. We know also from the proof of Lemma 1 that for every ME-deduction of a chain c there is an isomorphic GME-deduction of a generalized chain containing c. Hence the search space explored for find­ ing GME-refutations contains more redundancies, i.e. , paths leading to identical solutions. This is not critical, if one solution is looked for, as GME-refutations can be shorter. In such a. case a depth oriented search strat­ egy iR appropriate. H all solutions are looked for, it i11 necessary to employ a strategy that avoids exploring re­ dundant paths. The development of such strategies is one of the points that need to be investigated further.

GME may perform better than ME if the ressources for the search are restricted. E.g., if the search depth is limited, with GME more solutions can be f01md, as GME-refutations are shorter.

The generation of lemma should be restricted to the useful ones, since the addition of every new lemma. in­ creases the search space. Certainly, creating a. lemma candidate when performing an extension step with a1mit chain is superfluous, as the deduced lemma is an instance of the used auxiliary unit chain. Simple L-literals are in general less interesting than complex L-literals. There­ fore it may be reasonable to generate lemma. candidates only if the resolved literal in the auxiliary chain is a real complex literal.

However even the most useful lemmas introduce new redundancies into the search space, i.e., the same solu­ tion can be found by using a. lemma and by performing the extension and reduction steps that led to the de­ duction of the lemma. These new redundancies can be neglected, when only one solution is looked for, since it suffices to apply the lemmas first, before trying extension steps with non-unit chains.

When looking for all solutions, we have again the prob­ lem of avoiding paths leading to identical solutions. The situation becomes even more complex since the knowl­ edge base changes dynamically with the addition of lem­ mas. It may also happen that for finding all solutions, lemmas computed at another branch of the proof tree have to be used. Controling the generation and the use of lemmas is therefore another point that will be inves­ tigated further.

One pragmatic& solution would be to leave it to the user to decide when to apply a rule that lead to the introduction of a lemma. Like with the cut in Prolog, the user would be able to prune a part of the sear<.'.h space. The user has then the responsability for taking care that no solutions are lost.

In the LILOG project the knowledge engineers asked for such a feature. It happens often that a conjunction of literals should be treated as one literal. Introducing a new predicate symbol was not possible due to constraints imposed by the text understanding application. In such a case the solutions found by the use of lemmas were sufficient.

5 Conclusion

GME is a useful extension of ME. We have established some of its advantages and have pointed out areas of further investigation. Since GME applied to ordinary chains behaves exactly like ME, one has the flexibility to switch between GME and ME. The normalization proce­ dure has only to produce ordinary chains, and the com­ putational overhead for processing ME with the gener­ alized method is low.

An order sorted version of this calculus with lemma generation has been implemented in Quintus Prolog 4 for the LEU /2 text understanding system. GME has proven to be very useful, given the nature of the application domain, in which a majority of the rules written in the knowledge representation language LuLoG had conjunc­ tive conclusions.

Control issues have to be iuvestigated further. The major problem is how to avoid investigating paths in the search space that lead to redundant solutions. The generation of lemmas can be considered as a kind of rote learning. One may also think of storing certain lemmas permanently or of applying machine learning techniques like "explanation based generalizatiou" for creating more geuerallemmas. However, for avoiding the classical ma­ chine learuiug problem: "the more you know the slower you go", good strategies need to be developed for control­ ing the generation, the use and eventually the permanent storoge of lemmas.

Acknowledgements

I would like to thank Zuzana Dobcs, Karl Hans Blasius and Udo Pletat for helpful commeuts on this paper.