Extending Semantic Resolution via Automated Model Building: Applications

1 Introduction

Since the very beginning of automated theorem prov­ ing, researchers tried to put some semantics in theo­ rem provers in order to improve their power and effi­ ciency. (see for example [GELERNTER et al., 1983]) . This was a very natural idea: usually, human beings are strongly guided in their proofs by some interpretation of the conjecture they are trying to proof or to refute. But a problem immediately appeared: "how to formalize this idea ?" The first fully automated formal approach taking semantics into account was the set of support strategy [WOS et al., 1965] who was born almost simul­ taneously with resolution, and who is still considered as the most powerful restriction strategy available ([WOS,

Nicolas Peltier

LIFIA-IMAG 46, A venue Felix Viallet 38031 Grenoble Cedex FRANCE

Nicolas.Peltier@imag.fr

1988], page 52). In 1967, Slagle [SLAGLE, 1967] pro­ posed a very elegant and general restriction strategy for resolution, called semantic resolution, in which the ap­ plication of the resolution rule is controlled using ad hoc ground models given by the user. Slagle was aware of the limits of his method:

"A disadvantage of a semantic strategy is that the pro­ gram must at present be given a model along with the theorem to be proved. One might hope that someday the program could devise its own models" ({SLAGLE, 1961], page 695). ·

J. Slaney's SCOTT theorem prover [SLANEY, 1993] is an answer to this wish . SCOTT produces striking results using semantic resolution.

Slagle also emphasized the usefulness of models in im­ proving the set of support strategy:

"With set of support resolution, resolvents are gener­ ally not maximal and the underlying model is unknown. If the models were known many resolutions and resol­ vents could be eliminated" ({SLAGLE, 1961}, page 695).

The method we propose here overcomes the two draw­ backs pointed out by Slagle (for semantic resolution and set of support) . More precisely, we propose an extension of semantic resolution based on our former method for si­ multaneous search for refutation and model ([BOURELY et al., 1994; CAFERRA and ZABEL, 1992]) . It strongly relies on the use of constrained clauses, i.e. couples [clause : constraints] , instead of standard clauses . The constraints allow in some sense to code meta-reasoning: they are logical formulas imposing some conditions con­ cerning the inference rules.

Our approach has at least three important conse­ quences: first it prunes the search space for refutation in a similar - but stronger - way than semantic reso­ lution does. Second it allows to perform an incremental model construction. If a model of a formula F is known, and if we want to get a model ofF 1\ F', then our method computes the new model by extending the previous one, instead of re-computing it entirely. Last , but not least, it gives to all level of the support strategy a power similar to that of level 1.

The paper is divided into 5 sections. Section 2 recalls briefly the basic ideas of our method for model build­ ing and some of its key rules . In section 3 we propose an extension of semantic resolution and we prove its proper­ ties: soundness and refutational completeness. Section 4

is devoted to incremental model building: we state con­ ditions assuring that a model can be automatically built . One running example illustrates this construction.

Section 5 shows, via an analysis of the search space of the halting problem proof how our method prunes the search space of OTTER (if binary resolution is used) and produces a shorter proof.

2 Simultaneous Search for refutations and models

With the aim of increasing the possibilities of theorem provers as (hopefully intelligent) research assistants, we have developed few years ago a (refutationally complete) method combining search for refutations and models for first order formulas. The method captures the "normal" attitude of a human being faced to a conjecture: he con­ siders simultaneously two possibilities: to prove and to disprove the conjecture.

This method - called RAMC 1 - uses constrained clauses (or c-clauses), i.e. couples [clause :constraint]. Constraints code the conditions necessary either to the application or the impossibility of application of the in­ ference rules and denote the range of the variables of the clauses. It is neither possible nor useful to paste here large parts of results published elsewhere. Instead we recall some inference and disinference rules used in the examples that give also a taste of the method (for technical details see [CAFERRA and ZABEL, 1992] and [BOURELY et al., 1994]).

- The rule of binary c-resolution (abbreviated be­ resolution) on c1 and c2 upon lc (i) and l (s) is defined as follows:

- The rule of distautology generation imposes con­ straints on a c-clause in order to prevent it from being a tautology.

-The unit bc-dissubsumption rule imposes constraints preventing a c-clause from being subsumed by a unit c­ clause. It allows the elimination of the c-clauses that are logical consequences of other c-clauses of S. It is defined as follows (where x = var(X) U var(l(s))):

The binary-c-disresolution rule is a natural extension of the unit disresolution, defined in [CAFERRA and ZABEL, 1992].

where x = var(t2) U var(Y)

1 standing for Refutation And Model Construction

-The GPL-rule, ("Generating Pure Literal" rule) . Let S be a finite set of c-clauses. Let c be a c-clause in S and l be a literal in c. The GPL rule computes constraints for c in order to prevent application of be­ resolution upon l and lc (i.e. the complementary of l) between the c-clause c and any of the c-clauses in S.

Formally, let S be a set of c-clauses and c : [l(t) V c' : X] be a c-clause in S. The GPL-rule is de­ fined as follows:

where Xpure = 1\{\fil.[....,Yvs # t) : [k : Y] E S and zc(s) E k} 1\ X where yare the variables in var(Y) U var(k ).

In [BOURELY et al., 1994] the GPL rule is extended in order to deal with self-resolvent clauses. (it is easy to see that the result of the previous rule applied on self-resolvent clauses, is in most cases useless).

The reader can easily imagine the meaning of other rules of the method (based exactly on the same idea).

Our approach is not limited to Herbrand models: in [BOURELY et al., 1994], the method is extended to sets of equational clauses. We defined the c­ paramodulation and c-dis-paramodulation rules (similar to the c-resolution and c-disresolution rufe) and we give two termination criteria identifying classes of satisfiable equational unit clauses for which a model can be surely built . They allow to compute the domain D (a subset of the Herbrand universe) and to interpret function sym­ bols on the domain.

If RAMC stops, and if the set of c-clauses that we ob­ tain contains only unit c-clauses, it gives a model of the initial formula. The partial interpretation of the pred­ icates is given by the unit c-clauses produced by the method: each n-ary predicate P is mapped to two sub­ sets I(P)+ and I(P)- of Dn corresponding to the sets of n-tuples of ground terms for which Pis respectively eval­ uated to True and to False. The interpretation is partial because I(P)+ UI(P)- ~ Dn. If I(P)+ UI(P)- = Dn, we have a total interpretation of predicate P 2 · Obvi­ ously total interpretations are particular cases of partial interpretations. The sets I(P)+ and I(P)- are presently expressed by equational problems in an equational the­ ory. Equational problems are a decidable class of logical formulas quantified in a particular way and using only =, =f, 1\, V. We shall soon incorporate in the method con­ straints with more expressive power [PELTIER, 1995]. Interpretations (models) expressible by equational prob­ lems are called equational (or eq-) interpretations (mod­ els) .

3 Extending semantic resolution

The principle of semantic resolution [SLAGLE, 1967] is the following: it uses an interpretation I (given by the user) and prevents the application of resolution between two c-clauses that are true in I . This restriction is refu­ tationally complete. The main idea of the method we propose is a very simple one: since we are able to build models of sets of clauses, why not use them in order to guide research in similar way as semantic resolution (or the set of support strategy) does ?

2 Notice that not to be false in a partial model in not equivalent to be true in it

Immediately, we can go further: instead of evaluating clauses in a (in general partial) model, why not impose conditions- coded in the constraints- forcing a clause to be evaluated to false or not to be evaluated to false in the model ?

These simple ideas have important consequences: search space can be restricted with respect to that of semantic resolution and it gives to the method at all lev­ els a power similar to that of set of support at level 13. The model building capabilities of our approach are also improved, with respect to our previous work: we will show that the use of an interpretation I that is a model of some of the c-clauses makes the model construction for the whole set easier.

3.1 Semantic c-rules

We translate these ideas into the inference (and dis­ inference) rules of our method. Let I an eq­ interpretation, represented by a finite set of unit c­ clauses:

The variables of each c-clause [L;(s;) : X;] are de­ noted by y;.

If C : [V P; (ti) : X] then we note PI (C) the following equational problem:

It is easy to verify:

(i .e. there is a literal in C evaluated to true in I) . We introduce a new inference rule and a new disinference rule.

binary I-c-resolution :

Remark: -.PI ( c!) V ·PI ( c2 ) ensures that at least one of the c1, c2 will not be evaluated to true in I.

binary I-c-disresolution :

r1 : [L(t;} v R1 :X 1\ Y 1\ t1 = t2 1\ (-.P:r(cl) V -.P:r(c2))] r2 : [U(t;) v R 2 : X 1\ (vy.-.y v t1 f. t2 v (P:r(cl) 1\ P:r(c2)))] Theorem 1 Let I be an t~terpretatwn, S a set of cwhere y denote the variables of c 2 ·

r 1 and r 2 are two I-c-disresolvents of c1 and c2.

3 This corresponds to Wos 's wish in the first of his 33 basic research problem [WOS, 1988]

We shall call RAMCS the method RAMC augmented by the two rules above.

Remark: RAMC is a particular case of RAMCS, with I= 0 (i .e. I(P)+ = I(P)- = 0, for all P).

Notice that the use of equational problems allows to restrict the application of the resolution rule in a stronger way than semantic resolution, as defined by [SLAGLE, 1967] does, as showed by considering the fol­ lowing set of clauses:

and the Herbrand interpretation:

The following is a valid semantic derivation , according to Slagle's definition.

C4: S(x)

While RAMCS gives the following c-clauses:

The constraints of c5 have no solution and thus c5 can be removed from the set of c-clauses.

More precisely, it is possible to show that all the c­ refutations generated by our method do correspond to a ground semantic refutation (see theorem 1 below). This is not the case with semantic resolution: in previous ex­ ample, the first derivation did not correspond to any ground semantic derivation (for more details about this problem, see for example [McCUNE and HENSCHEN, 1985]).

In [STANDFORD, 1980], a method was proposed in order to avoid inferences that do not correspond to any ground inference: it attaches to each clause a list of lit­ erals whose descendants must be falsified (it was called the FSL list). This method appears to be not efficient [McCUNE and HENSCHEN, 1985] .

"The FSL method was implemented but during pre­ liminary experiments we found that it required too much processing time. During deep searches the FSL lists be­ came very long and the improvement was small or non­ existent." ({McCUNE and HENSCHEN, 1985], page 256)

Our approach seems to be more adapted to solve-this problem in a more natural and efficient way.

In theorems and lemmas below "interpretation" means peq-interpretation.

. . clauses and d be a dertvatwn from S usmg the I-c­ resolution rule. Let d' be a corresponding ground deriva­ tion (i.e. d' = CTgr(d)). Then d' is a ground semantic derivation from ground instances of c-clauses in S.

Proof 1 By induction on the length n of d:

• If n = 0, the theorem obviously holds
• Assume that the theorem holds for n . Let d be a derivation of length n + 1. The first step of d is of the form S -r S U { R}, where R is of the form:

and there exists c1, c2 E S such that:

The first step of d' is of the form:

where u E Sol(X 1\Y/\tl = t2/\(-,Px(cl)V-,Pz(c2))). O" rt Sol(Pz(cl)) orO" rt Sol(Ez(c2)). hence: I ~ u(L(tl) V R 1) or I~ u(-,Lc(l2) V R2). At least one of the two parent clauses is false in I. The first step of d' is therefore a ground semantic inference. Using induction hypothesis, we deduce that d' is a ground semantic derivation.

3.2 Soundness and Refutational Completeness of the method

Theorem 2 (Soundness) Let c1 and c2 be two c­ clauses, let I be a interpretation, r a binary I -c-resolvent of c1 and c2, r1 and r2 the binary I-c-disresolvents of c1 and c2 . Then:

• r is a logical consequence of r1 and r2.
• c1 1\ c2 = r1 1\ r2 1\ c2 i.e. c1 can be deleted from the set of c-clauses and replaced by r1 and r2.

Proof 2 The proof is similar to those of lemmas 9.1 and 3.6 in [CAFERRA and ZABEL, 1992).

The proof of refutational completeness needs the fol­ lowing lemma:

Lemma 1 Let I be a partial interpretation I . Then there exists a total interpretation I' such that, for all ground clause C:

Proof 3 Let I be a partial interpretation. Let I' be the interpretation defined by, for all predicate P (D is the domain ofi):

Let L(l) a ground literal. If L is positive we have: 1 f= L(l) ifft E I(P)+ i.e. l E I'(P)+, hence I' f= L(t). If L is negative, I f= L(l) implies I ~ £C(l), hence 1' ~ £C(l) (since Lc is positive) and I' f= L(l) (since I' is total) .

Then for each ground clause C = V7=1 L;(ti), we have:

1 F= c iff:

• 3i .I f= L; (ti), then I' f= L; (ti) and therefore I' f= c
• or 3i,j.Li(ti) = Lj(tj) , then I' f= C (Cis a tautology).

Lemma 2 (Lifting lemma)

Let [C1 :XI] and [C2 : X2] be two c-clauses, o-1 and o-2 solutions of X1 and X2 respectively, I a interpreta­ tion, I' the total interpretation as in lemma 1, and R 9 a I' -resolvent of o-1 ( C1) and o-2( C2). Then there exists a I-c-resolvent [C : Y] of [C1 : X1] and [C2 : X2] and a solution O" of Y such that u(C) = R 9 .

Proof 4 Let c1 : [L(ll) V R1 : X1] and c2 : [Lc(t2) V R2 : X2] be two c-clauses, o-1 E Sol(XI), o-2 E Sol(X2), I a interpretation.

Let R 9 a I-resolvent of u!(L(tl) V RI) and o-2(Lc(t2) V R2).

Let R : [ C : Y] be the I' -c-resolvent of c1 and c2. Let u = o-1 U 0"2. We have u E Sol(X1 1\ X2). Moreover o-1(tl) = o-2(t2), hence u E Sol(X1 1\ X2 1\ t1 = t2).

R 9 is a I'-resolvent of o-1(L(tl) V R1) and u2(Lc(t2) V R2), therefore we have either I' ~ 0"1 (L(tl)V RI) or I' ~ u2(Lc(t2)V R2) By lemma 1 we have: I~ u!(L(tl)V R!) or I ~ o-2(Lc(t2) V R2) i.e. o-1 E Sol(Px(c1)) or o-2 E Sol(Pzc2) .

Hence u E Sol(Y) .

Theorem 3 (Refutational Completeness)

For all interpretation I and for all unsatisfiable set of c-clause S there exists a refutation of S using only I-c­ rules.

Proof 5 By refutational completeness of semantic res­ olution [SLAGLE, 1967] there exists a ground I'­ refutation of S. By lemma 2 it can be lifted to non ground c-clauses, to obtain a I-c-refutation of S.

4 Incremental Model building

One of the most interesting features of our method is that it allows building models incrementally. This char­ acteristic is particularly interesting when dealing with large sets of clauses (databases, ... ). The following the­ orem gives conditions allowing to extract a model from a set of c-clauses obtained when RAMCS stops. This conditions are similar - but weaker - than those for RAMC (the former conditions imposed that all c-clauses had to be unit c-clauses). Therefore RAMCS is stronger than RAMC. Indeed, we take advantage of the inter­ pretation I that is already a model of a some of the c-clauses, in order to compute the whole model as an extension of I.

Theorem 4 If S is a set of c-clause stable by all the rules of RAMCS, and if all non unit c-clauses of S are true in I, then a model of S can be automatically com­ puted.

Proof 6 Let S be a stable set of c-clause, such that all non unit c-clause of S is true in S.

The interpretation I' is defined as follows: For all ground term l:

We prove that I' I= S, by case analysis on the length of the c-clauses.

For all c-clause c: [V7=l L;(fi) :X] E S we have:

• if n = 1 (C is a unit c-clause), then Vu E Sol(X).I' I= L;(u(4)) (by definition ofi').
• if n > 1, then C is true in I'. Let u E Sol(X). Then, since C is stable by distautology, there exists i such that u( L; (4)) is true in I . Since S is sta­ ble by unit-c-I -disresolution, for any unit c-clause [L;(s) : Y] , we have: Y 1\ X 1\ s = 4 = 1.. Finally, by definition of I', we have: I' I= u( L; (4)), and

Remark: RAMCS allows therefore to perform an in­ cremental model construction: the model I' in the proof above is built by modifying and extending the previous one. As already pointed out, this feature is especially useful when the set of c-clauses S is very large (for ex­ ample in databases), and when the adding of the new c-clauses does not modify radically the intended mean­ ing of S .

Example

The following example, taken from [FERMULLER et al., 1993], illustrates the model building aspect of RAMCS.

1 [] [[ P(x) I Q(g(x,x)) : TRUE ]] . 2 [] [[ -Q(x) I R(y,x) : TRUE]]. 3 [] [[ -R(a,a) I -R(f(b) ,a) : TRUE]]. 4 [] [[ R(f(x) ,y) : TRUE]]. 5 [] [[ P(x) I -P(f(x)) : TRUE]]. 6 [] [[ -P(a) : TRUE ]] .

RAMCS builds automatically the following Herbrand model.

4 [] [[ R(f(x),y): TRUE]]. 9 [gpl] [[ Q(g(x,x)) :TRUE]]. 12 [gpl] [[ -R(a,a) : TRUE]]. 10 [gpl] [[ -Q(a) :TRUE]]. 11 [gpl] [ [ -P (f (x)) : TRUE ]'] . 6 [] [[ -P(a) :TRUE]]. 13 [gpl] [[ R(x,y) : ((a != y) I (a != x)) ]] .

Then suppose we add the following c-clauses:

7 [] [[ -S(x) I S(g(x,x)) : TRUE ]] . 8 [] [ [ S (a) I S (f (x)) : TRUE ] ] . 9 [] [[ -S(x) I -R(b,g(x,x)) : TRUE ]] .

RAMCS gives (with the previous model).

10 [resolution,9,7] [[ -S(x) I -R(b,g(x,x)) :TRUE]]. 11 [resolution,10,7] [[ -S(x) I -R(b,g(g(x,x),g(x,x))) :TRUE]]. 12 [resolution,11,2] [[ -S(x) I -Q(g(g(x,x),g(x,x))) :TRUE]] . 13 [resolution,12,1] [[ -S(x) I P(g(x,x)) :TRUE]]. 14 [gpl] [[ P(g(x,x)) :TRUE]]. clause #13 is deleted by dissubsumption 14,13. 15 [dissubsumption,14,1] [[ P(x) I Q(g(x,x)) : (x != g(y,y)) ]] . 16 [gpl] [[ -Q(g(g(x,x),g(x,x))): TRUE]]. clause #12 is deleted by dissubsumption 16,12. 17 [dissubsumption,16,2] [[ -Q(x) I R(y,x)

: (x != (g(g(z,z) ,g(z,z)))) ]] . 18 [gpl] [[ -R(b,g(g(x,x) ,g(x,x))) : TRUE]]. clause #11 is deleted by dissubsumption 18,11. 19 [dissubsumption,18,10] [[ -S(x) I -R(b,g(x ,x)) : (x != g(y,y)) ]] . 20 [gpl] [[ S(g(x,x)) : TRUE]]. 21 [gpl] [[ S(a) : TRUE]].

Here we get a set of c-clauses satisfying the conditions of section 4, and the model is:

% modified previous literals [[ R(f(x),y) : TRUE]]. [[ Q(g(x,x)) : (x != g(y,y)) ]] . [[ -R(a,a) :TRUE]]. [[ -Q(a) :TRUE]]. [[ -P(f(x)) :TRUE]]. [[ -P(a) :TRUE]]. [[ R(x,y) : (all z ((a != y) I (a != x)) & ((x !=b) I (y != g(g(z,z),g(z,z))))) ]] . % new literals 14 [gpl] [[ P(g(x,x)) :TRUE]]. 16 [gpl] [[ -Q(g(g(x,x),g(x,x))) TRUE]]. 18 [gpl] [[ -R(b ,g(g(x,x) ,g(x,x))) : TRUE]]. 20 [gpl] [[ S(g(x,x)) :TRUE]]. 21 [gpl] [[ S(a) : TRUE]].

Remark 1: for the sake of clarity, we let the con­ straints of R(x,y) in unsolved form (i.e. in non canoni­ cal one). its solved form would be (after elimination of parameter z):

[[ R(x,y) : (((a != y) I (a != x)) & ((x ! = b) I (y = a) I (y = b) I (y = f (z)) ((y = g(u,v)) & ((u != v) I ((u = a) I (u =b) I (u = f(v1)) I ((u = g(v1,v2)) & (v1 != v2))))))).

Remark 2: the model built by RAMCS is infinite.

The next section is devoted to the detailed analysis of a non trivial example in which, in addition to the pruning of the search space allowed by RAMCS , we show a nice side effect of its application: the possibility of finding shorter proofs.

5 Pruning the search space and shortening proofs: an example

To prove that a set of c-clauses S implies a conclusion C, we use - according to the ideas introduced in section 3 - the following procedure:

1. Compute a partial model M of S. 2. Use M-e-rules on S U ...,c.

The first step may of course not stop (first order logic is undecidable) , hence we have to fix a limit on the search for M (for example an upper bound on the number of c-clauses generated or on the search time ... ) , in order to keep refutational completeness. This is similar to what is done in SCOTT [SLANEY, 1993]. Nevertheless, even if we do not get a model of S, we will get a model of a subset of S, that can be use in step 2 (in the worst case M will be empty).

It should be remarked that the use of partial models allows a finer and more dynamic control of the applica­ tion of resolution rule because it can be enriched as the search for refutation goes along.

A problem we consider related to the use of seman­ tic notions in theorem proving is the one of finding shorter proofs. This problem became to be an important one in automated deduction. Obviously, an exhaustive, breadth-first search (ensuring that the shortest proof will be found) is in general impossible. Sometimes the use of semantic notions as in our method allows to find short proofs in a reasonable time.

The halting problem

This fundamental problem in Computer Science is an interesting challenge for automated theorem provers, es­ pecially for those using resolution (for one of the usual formulations in the automated deduction literature there is no known fully automated resolution proof [DAFA, 1994]).

The formulation we consider in this section is the one of M. Bruschi [BRUSCHI, 1991] 4 .

With this formulation, M. Bruschi obtained a 26 steps proof of the theorem, using ENprover, the DSI imple­ mentation of the Hsiang's EN-strategy method. He used a breadth first strategy with set of support.

RAMCS builds the following model M of the hy­ pothesis ( without the denial of the conclusion):

1 [] [[ -algorithm_program_decides(A) : TRUE]]. 2 [] [[ -program(A) : TRUE ]] . 3 [) [[ -program_program_decides(A) :TRUE]]. 4 [] [[ -program_halts(A,B) :TRUE]]. 5 [] [ [ -algorithm (A) : TRUE ] ] . 6 [] [[ -program_halts_halts2_outputs(A,B,C,D) :TRUE]]. 7 [] [[ program_decides(A) :TRUE]]. 8 [] [[ -halts2_outputs(A,B,C,D) : TRUE]). 9 [] [[ -program_not_halts(A,B) : TRUE ]] . 10 [] [[ -program_not_halts_halts2_outputs(A,B,C,D) : TRUE ]] . 11 [] [[ -program_not_halts_halts2_outputs(A,B,C,D) :TRUE]]. 12 [] [[ -program_not_halts_halts_outputs(A,B,C) : TRUE ]] . 13 [] [[ -halts_outputs(A,B,C) :TRUE]]. 14 [] [[ -program_halts_halts_outputs(A,B,C) : TRUE ]] . 15 [] [[ -outputs(A,B) : TRUE ]] . 16 [] [[ -program_not_halts_halts_outputs(A,B,C) :TRUE]].

Once we have a model we can use RAMCS. The proof obtained by RAMCS using the model M is (input c­ clauses are distinguished by the "[ ]" prefixing them):

11 [] [[ -program_halts(A,B) I halts(A,B) :TRUE]]. 17 [] [[ -program_not_halts(A,B) I -halts(A,B) : TRUE ]] . 22 [] [[ -program_halts_halts2_outputs(A,B,C,D) I program_halts(B,C) :TRUE]]. 25 [] [[ -program_not_halts_halts2_outputs(A,B,C,D) I program_not_halts(B,C) : TRUE]]. 34 [) [[ -algorithm_program_decides(A) I program_progr~_decides(c1) : TRUE]].

4 taken from the TPTP library, problem COM003-2, see there the initial set of clauses

35 [] [[ -program_program_decides(A) I program_halts_halts2_outputs(A,B,C,good) :TRUE]]. 36 [] [[ -program_program_decides(A) I program_not_halts_halts2_outputs(A,B,C,bad) :TRUE]]. 43 [] [[ algorithm_program_decides(c4) : TRUE]]. 44 [resolution,43,34] [[ program_program_decides(c1) :TRUE]]. 50 [resolution,44,36] [[ program_not_halts_halts2_ outputs(c1,A,B,bad) :TRUE]]. 52 [resolution,44,35] [[ program_halts_halts2_ outputs(c1,A,B,good) : TRUE]]. 79 [resolution,50,25] [[ program_not_halts(A,B) : TRUE ]] . 83 [resolution,52,22] [[ program_halts(A,B) :TRUE)]. 88 [resolution,83,11] [[ halts(A,B) :TRUE]]. 133 [resolution,79,17] [[ -halts(A,B) :TRUE]]. 134 [resolution,133,88] [[ :TRUE]).

OTTER [McCUNE, 1990], using binary resolution and set of support strategy, produces a 12 steps proof, after generation of 90 clauses. The proof found by RAMCS is 8 steps long. The proof has therefore been shortened by 33%.

Discussion

Globally (i.e. for refutation and model building) our method generates 134 c-clauses, OTTER generates 90. In fact, when comparing the two methods, one should keep in mind than we apply simultaneously refutation and model building rules. So, for each clause generated by resolution, 2 or 3 c-clauses are generated by c-resolution and c-disresolution rules. If we consider only refutations rules RAMCS generates only about 50 c-clauses. The search space for refutation is therefore reduced by almost 50%. Computing time is roughly the same.

Of course, when looking only for refutation , the "model building rules" flag can be turned off and the search space is the refutation search space in the usual sense, which is reduced in this example by 45% with re­ spect to that of OTTER.

Remark: the model building task performed by RAMCS can be consider as automated meta-reasoning done in the object level.

6 Conclusion and future work

We have extended semantic resolution and as side effect we have also improved the set of support strategy us­ ing a method for incremental automated construction of (finite or infinite) models.

Two points will be studied in the .near future.

• The first one is a practical one, i.e. we shall exten­ sively experiment our method on more complicated examples, particularly on open problems. For exam­ ple, we shall look for a mechanical solution of the halting problem using the specification for which no fully automated resolution proof is known.
• We shall study the extension of our method to se­ mantic paramodulation.