Sub-problem Finder and Instance Checker: Two Cooperating Preprocessors for Theorem Provers

SUB-PROBLEM FINDER AND INSTANCE CHECKER

TWO COOPERATING PREPROCESSORS FOR THEOREM PROVERS

Dennis de Champeaux Bedrijfsinformatica University of Amsterdam Jodenbreestraat 23 K3123

1011 NH Amsterdam

Two pre-processors for theorem provers are described, which when applicable, will lead to search space simplification.

Both were implemented and integrated with an existing resolution type connection graph theorem prover.

Examples are provided which confirm our claim of search space simplification. Key words and phrases: Theorem proving, pre-processing, search space simplification .

.!..:_ Pre-processors for theorem provers in general.

The main paradigm in automatic theorem proving is or should be that search is to be avoided, postponed, or else to be minimized. This should be done by any means one can lay one's hand on while maintaining completeness, generality and not succumbing to the ad-hocness as advertised by the proceduralists.

Search space simplification has been a major goal in the resolution school. Exploiting 'larger' more numerous operators (derivation rules) is the main activity in the natural deductionschool. There are however many more options to be de­ veloped with which the role of search can be limited to those circumstances where there is

no sensible alternative.

Already slumbering for some years is the applica­ tion of multi-level search in theorem proving (Sacerdoti, 1973 [7]). It is incomprehensible that the support from a model technique (Gelern­ ter, 1959 (3]), has not been pursued. Search guidance w1th heuristic functions and automatic improvement of them is still inconclusive, al­ though it has become clear that syntactic features can contribute only modestly to such functions. Chosing an appropriate representation (within one language say predicate calculus) is a wide open problem. Determining the right re­ presentation language is not yet a problemsince it is not known whether multiple representation languages are necessary.

The former two issues belong to the preprocessing repertoire. We mention a few more. Selection of

relevant axioms and/or definitions and/or already proven theorem/lemmas to prove a conjecture; finding a counter example of a conjecture to make sure that a proof is impossible; finding a similar already proven theorem to see whether its proof can be generalized and/or modified to handle a conjecture; instantiating a secondorder­ theorem (e.g. induction scheme); reducing a con­ jecture to independent sub-problems (reduction to weakly dependent sub-problems can be done in the multi-level search framework); recognizing that a conjecture is an alphabetic variant and/ or an instantiation of an axiom or an already proven theorem; etc.

This paper reports the results of implementing the two last mentioned. The next sectiondescribes the independent sub-problem recognizer. Section 3 deals with the instance checker. Section 4 dis­ cusses how they are cooperating and how they should be related from a process point of view. Two ex­ amples are given in section 5.

2. The independent sub-problem recognizer.

The sub-problem recognizer we developed is based on components of a predicate calculus-conjunctive normal form translator. Our translatorwas inspired by the procedure as described in Eanna, §. A small improvement to this translator led to sub-problem decomposition. First we present the original translation. Then we expand one of the steps (as was also partially done in [!.oveland, ~page 34). A subset of these translator rules make up the sub-problem recognizer.

The translator in [Manna, ~ omitting here ir­ relevancies, consists of the following steps:

1- Eliminate 'if .·. then' and 'if and only if'. Replace A)B by V(~A,B), and A=B by A(V(~A,B), V(A,~B)). 2- Move 'not' inwards. Replace ~(x)A by (ax)~A, ~(3x)A by (x)~A, ~V(AI, ·.. , An) by A(~AI, ..· , ~An), ~A(AI, .·. , An) by V(~AI, ·.. , ~An), and ~A by A. 3- Push quantifiers to the right. Let (Qx) be (x) or (3x), and let XX be A or V ; replace (Qx) XX (A I, . . . , Ai, .· · , An) by >O<{Ai, (Qx)XX(AI, ·.. ,Ai-I,Ai+l, ... ,An)} if x not free in Ai. 4- Eliminate existential quantifiers (introduc­ tion of Skolem functions). Pickout the left­ most well formed part (3y) (B(y)) and replace it by B ( f (xil, ... , xin)) where a) Xi, ··. , Xin are the free variables of (ay) (B(y)) which are universally quantified to the left of (ay) (B(y)); b) f is a 'fresh' n-ary function constant. 5- Eliminate universal quantifiers. 6- Distribute 'and' over 'or'. Replace V(AI, ·.. , Ai, A(BI, ··. , Bk), Ai+l, ... , An) by A{V(AI, ... , Bl, ... , An), ... , V(AI, ... , Bk, ... , An)}· If step (i) can be reapplied it has precedence over step (i+l). Remark: A sequence of say universal quantifiers should get special attention in step 3. E.g. (x)(y){VP(x,y), Q(y)} can be replaced by (y)V{Q(y), (x)P(x,y)}· Thus every universal (existential) quantifier in a sequence of universal (existential) quantifiers should be moved to the right of the sequence in its turn to check whether it can be pushed further to the right. This procedure can be improved by expanding step 3 with: 3.1 Straighten out 'and's and 'or's. Let )()( be A or V. Replace l«(AI, ··. , Ai, >O<(BI, .·. , Bk), Ai+l, . · . , An) by )0( (A I , ·.. , Ai , B I , ··· , Bk, Ai+l, ... , An). 3.2 Distribute 'and' over 'or' or vice versa. Replace (x)V(AI, ··· , Ai,A(BI, · ·· , Bk), Ai+l, ... , An) by (x)A(V(AI, ... , Bl, ... , An), ... , V(AI, ... , Bk, .· .. , An)) and (h)A(AI, ·.· , Ai,V(BI, ··· , Bk), Ai+l, .. . , An) by (3x)V(A(AI, ... , Bl, ... , An), ... , A(AI, ... ,Bk, ... ,An)).

3.3 Distribute quantifiers over connectives. Replace (x)A(AI, ... , An) by A((x)AI, ... , (x) An) and (3x)V(Al, . , · , An) by V( (3x)AI, ... , (3x)An). Example: Using the extended step 3 the formula : (x) J! (x)A(y) { Q(x, y) A ( 3z) R(y, z) [! can be rewritten into: (x)P(x)A(y)(x)Q(x,y)A(y)(3z)R(y,z) . Observe that this replacement simplifies the Skolem function that has to be generated fo r the elimination of the (3z)-quantifier. Remark: It is worthwhile to check for redundan­ cies (using the instance checker) after applica­ tion of step 3.2. E.g. V((x)A(x), A(a), ... )can be simplified to V(A(a), ... ) while A( (x)A(x), A(a), ... ) can be replaced by A((x)A(x), ··. ) . Remark: For easy readability we used in 3.3 the same variable 'x' in all the terms of the con­ nective in the replacement. This does not hur t the translator. The instance checker however can get confused and demands step 3.3 to be mo­ dified such that each term in the replacement has a new fresh variable.

The INdependent SUB-problem REcognizeR- INSURER ­ consists of step I upto the modified step 3 and with step 6 . It is obvious that in case INSURER applied on a problem P produces a form with lead­ ing connective 'and' its terms are independent sub-problems and if all sub-problems can be proven the P has been solved. The reverse statement that INSURER will find a maximal decomposition if P can be decomposed we leave as an intriguing t ask for Aiello/Weyrauch's program FOL [1].

We end this section with the 'real-life' examp le given in box I.

(I) (x)(y)(z) x(yz)a(xy)z (2) (x) xe·x (3) (x) ex=x (4) (x) xi(x)=e (5) (x) I(x)x=e (6) (H) (SUBGR(H)+-+{ (3x)H(x)A (x) (y) (!i(x) AH(y)-+H(xy[j A (x)(H(x)-+H(I(x)))}) (7) (HI)(H2){SETEQ(HI,H2)+-+(x)(HI(x)+-+H2(x))} (8) (g)(xx)(H)(COSET(g,xx,H)+-+ {SUBGR(H)A (x)(xx(x)+-+(3y)(H(y)Ax·yg)) }) (9) (g) (xx) (H) (COSET(g,xxH)-+{H(g)+-+SETEQ(xx,H)}) . box I Axioms (1-5), definitions (6-8) and a theorem (9) from group theory.

(1-5) are non-minimal axioms defining a group; (6-8) are definitions of respectively sub-groups, equality of subsets and of right-cosets; (9) is a theorem expressing a property of cosets.

Observe that subsets are represented by !-argu­ ment first order predicates, and that SETEQ and COSET are 2nd order predicates. Direct transla­ tion of (1-8) and the negation of (9) into con­ junctive normal form yields 39 clauses with to­ gether 109 literals.

INSURER however recognizes that (9) can be de­ composed into:

Working on (10) (not done by INSURER, but by an­ other program component) the definition of COSET, SETEQ and SUBGR are respectively substituted. The result is negated and together with (1-5) translated into conjunctive normal form yielding 14 clauses with 23 literals. After each substitu­ tion of a definition INSURER is called to check whether further decomposition is possible. When working on (II) this strategy is succesful after substituting away SETEQ. Two new sub-problems are found both ending up with 14 clauses and 21 literals.

Although our connection graph theorem prover COGITO is not yet able to handle these three sub-problems, the chance to find a solution has increased with an 'infinite' amount when compared to the non-decomposed situation.

INSURER also can handle the sorted predicate cal­ culus that was introduced . in @hampeaux, ~. The same coset example formulated 1n sorted predicate calculus - without decomposition - yields 28 clauses with 61 literals. INSURER finds here al­ so three sub-problems each having 12 clauses with respectively 16, 14 and i4 literals. A sig­ nificant reduction again, possibly bringing this problem within reach of the with paramodulation extended COGITO.

3. The instance checker

The instance checker (INSTANCE) we designed and implemented is in fact a special case theorem prover. It is an instrument with which a conjec­ ture can be recognized as being an alphabetic variant or as a special case of an already ac­ cepted theorem. Conjecture and theorem are ex­ pressed as closed, slightly restricted - see below- predicate calculus formulas.

Le t T and K be respectively a conjecture and an accepted piece of 'knowledge'. The input of the

• recursive INSTANCE consists of three elements: two forms T and K for which must hold that they do not share variables and that dis­ regarding permutations of sequences of quan­ tifiers and/or arguments of 'and' and 'or' it is the case that T · INSURER(T) and K · INSURER(K); and
• a list of variables, VR, to be explained in the sequel, which at the top level call is empty.

Although at the top level one is mostly interest­ ed in a yes-no answer, for reasons that should become clear in the description of INSTANCE, the output is more substantial in the positive case. The output of INSTANCE is:

• NO, signifying that T is not an instance of K, or else
• a list of triples, where each triple is of the form {a, Tcr, Kcr} with cr a substitution, Tcr a "without loss of generality substitution instance" of T being a logical instance of the special case Kcr of K. It should now be clear that if NO; INSTANCE(T,K,~) then K~T.

An example where more than one triple will be returned by INSTANCE is:

T = (lx)Ax,x), K- (y)(A(p,y)AA(q,y)), with the output: ({;:~. A(p,p), A(p,p)AA(q,p)} {~, A(q,q), A(p,q)AA(q,q)})·

We give a simplified description of INSTANCE omitting subtilities that have to do with the equality predicate, e:e:y stands for: the identifier et occurs in the expression y; Sey is the result of substituting et for B in the expression y; thus S~y = ycr when cr={S+a}·

We assume that the employed unification algo­ rithm is willing to accept also non-literal pre­ dicate calculus formulas and so we get for exam­ ple {z+a} when calling UNIFY( (x)A(x,a), (x)A(x,z), {z}fl· INSTANCE(T,K,VR):= - if T and K are unifiable, taking into account VR, under substitution cr then return with ({cr, To, Kcr}) else if K = (et)(Form(et)) then U:=INSTANCE(T, Form(et), VRU{et}) if U=NO then return with NO else else ~hus Us~{cri,_xi· Yi}) return ~{cri, xi, YiJ, where Yi=(et)Yi when CLE:Yi or else Yi if T = (3et)(Form(et)) then U:·INSTANCE(Form(et), K, VRU{et})

if U·NO then return with NO else return ~{oi, Xi· Yi} where Xi=<:1a)xi when Cl£Xi or else Xi else if T (a)(Form(a)) then let c be a fresh constant U:ziNSTANCE(S~(Form(a), K, VR) if U=NO then return with NO else return ~{oi, Xi, y·} where xi=(a)S~xi when c¢Yi or else Xi else if K (a a) (Form(a)) then else let c be a fresh constant U:·INSTANCE(T, s& Form(a), VR} if U·NO then return with NO else return ~{oi, Xi· Yi where Yi =(a a) S~Yi when c~xi or else Yi if K · V(K1, ... , Kn) then return ~{oi, xi, Yi}where Xi·TOi, yi·KOi and fohr al~ j xi i_s an ins~nce of Kjeri or if no sue trlple ex1sts NO ~ee the appendix for a more detailed descr1ption of this cas~ if else T = A(Tl, ·. ~· Tn) then return 1 {oi, xi, Yi} where Xi·Tcri, Yi=KOi an~ for all j TjOi is ~n instance of Yi ~r 1~ no such tnple exuts NO ~e omit spec1f1cat1on of this case since it runs parallel to the former cas~ else if T = V(Tl, .·· , Tn) then U: = ~ for all T· do U2:·INST~CE(T·, K, VR) if U2j~NO thus H~·~{cri, Xi, yi} then U:·UUi{oi, Toi, Yi} if U=~ then return NO else return U else if K = A(Kl, ··· , Kn) then U: = ~ for all K· do U2: =INStANCE(!, K·, if U2j~NO then U: · OU else return NO. VR} ~{oi· xi, Koi}

As mentioned in the former section INSTANCE is called in INSURER after application of step 3.2. The effectiveness of doing so was proven by the conjecture of the second example in section 5: (x) (ay) {A(Equal(x,nil) .·. Without INSTANCE INSURER will decompose this example into eight (8:) sub-problems of which six are redundant. When INSTANCE is incorporated the two non­ redundant sub-problems only remain. INSURER and INSTANCE can also be coupled in another way as we will describe in the next section

~ Interplay between INSURER, INSTANCE and COGITO and what is to be desired. --

INSURER, INSTANCE, COGITO and the predicate cal­ culus - conjunctive normal form translator - were embedded in a 'fixed' regime. Input for the prover consists of axioms, supporting theorems, definitions and the conjecture. For the next des­ cription we want t9 remind that activation of the connection graph theorem prover COGITOshould be postponed at all costs.

Roughly a supervisor triggers the following acti­ vities:

• step 1: If the conjecture is an instance of an axiom, a theorem or an already proven theorem (see step 2) then return with success.

step 2: If the conjecture decomposes into the

sub-problems Cl, ·.. , Cn

then for each Ci go (recursively) to

step I if th~ value returned for

treating

Ci is succesful

then add Ci to the collection of

already proven theorems

else quit with failure

return with success.

• step 3: If the conjecture contains a predicate defined in one of the definitions then substitute for each occurrence in the conjecture the instantiated body of the definition· and go to step 1.
• step 4: Translate the axioms, supportingtheorems and the negation of the conjecture into conjunctive normal form, call COGITO and return the value returned by it. (COGITO gets a resource parameter ensuring ter­ mination).

The results reported in the next section have bee~ obtained with this, slightly different, reg1me. Although this particular fixed connection between INSURER, INSTANCE and COGITO makes sense and is certainly effective we do not like it. We prefer considering INSURER, INSTANCE and COGITO as being members of a potentially larger family of deductive, cooperating, independent specialists. This would require the supervisor to be implement­ ed as a multi-processes scheduler. The overall str~cture would be more transparant, making more eas1ly addition of a new specialist. Not having available language as QLISP, INTERLISP and MAGMA­ LISP prevented us of doing so.

~Examples

Our first example looks terribly simple but a straightforward treatment after translation, by COGITO had not yet found a contradiction after generating 35 clauses. It consists out of only: de finition: (s)(t){SETEQ(s,t)++(x)(xEs++xEt)} and conjecture: (u)(v){SETEQ(u,v)++SETEQ(v,u)}· INSURER immediately recognizes that the con­ jecture decomposes into two sub-problems of which INSTANCE shows that one is an alphabetic variant of the other. Remains to be proven:

· Recursive definitions are not allowed

(u)(v){~SETEQ(u,v)VSETEQ(v,u)}·

After substituting away SETEQ with the defini­ tion INSURER finds again two sub-problems and - surprise - INSTANCE also finds that one is a variant of the other. Remains this time:

(u)(v){ V(3yl)(ylEvAyl~u)

(3y2)(y2~vAy2Eu)

(y3)(y3EvVy3~u) ·

Nega ting this conjecture and translating into C.N.F . yields four clauses. The 2nd clause ge­ nerated by COGITO was already the empty one. Generating the non-solution with 35 clauses was 20 times more costly than finding this solution.

The next example was taken from @reen, ~ and was already worked on as reported in ~hampeaux,]. definition: (x)(y){R(x,y)+-->(Same(x,y)J\Sd(y)). axioms: (I) (x) (y){Sd(y)-+Sd(merge(x,y))}, (2) (x)(y)(u){(Sd(y)ASame(x,y))-+ -+Same(cons(u,x), merge (u,y))} , (3) (x) {Equal (x,nil)-+R(x,nil) , (4) (x) {~Equal (x,nil)-+ -+Equal(x, cons(car(x)cdr(x)))}, (5) (x)(u)(v){Equal(x,u)ASame(u,v)-+Same(x,v)}· conjec ture: (x)(3y){(Equal(x,nil)-+R(x,y))A (((~Equal(x,nil))A · R (cdr (x) , sort (cdr ( x)):))-+ -+R (x,y))}·

The conjecture - already mentioned in section 3decomposes into two sub-problems of which INSTANCE finds that one is an instance of axiom(3). The remaining s ub-problem was solved as well as without definition substitution (by adding the definition to the axioms) as with substitution. In both cases a contradiction was found more easily than i n the non-decomposed case as can be seen from the g-penetrance values in table I.

Table I Showing the effectiveness of INSURER and INSTANCE. The numbers between brackets refer to values obtained when the sorted predicate calculus is used @hampeaux, ~. (The g-penetrance is def1ned as ~ clauses in proof/ * (input+generated clauses).)

6 . Summary

Two algorithmic (always halting) components from the natural deduction realm are described. Both were implemented and integrated as pre-processors with a resolution type, connection graph theorem pDover. Examples are given that illustrate augmented power of this complex with respect to the sole theorem prover.

Factoring out other algorithmic components and/ or adding plan/strategy generators to the pre­ processor family (possibly leading to multi-level search [sacerdoti, fl, we consider a more promis­ ing future task than investing more intelligence deep inside resolution and/or natural deduction theorem provers.

Excellent typing was done by Porn van der Horst

Appendix

We give here a more detailed description of the sub-case INSTANCE(T, V(Kl, ... , Kn), VR). INSTANCE(T, V(Kl, ·.. , Kn), VR):= INSORK(({(Kl, ... , Kn)(0,T,0})) So we have now to describe the procedure INSORK. Its input consists of a non-empty list (Taskl, ..· , Taski, .·. ),where an element Taski is of the form: {(Rm, ... Rn)(cr, T, (Rl, ... , Rm-1))}, with Rj=Kjcr, T=Tcr. rt is already an instance with respect to V(Cl, ... , Rm-J)j INSORK(~ Taski):= Newtask : .. 0 for each Taski do U:=INSTANCE(T, Rm, VR) if u;NO thus U=U{crj, Xj· Yj} then for each element of U do NN:={(Rm+lcrj, ... , Rncrj) (cr+crj, xj, (Rlcrj, ... , Rm-loj·Y))J Newtask:·NewtaskUNN if Newtask=0 then return NO if m·n thus all elements Ki have been treated then U2:=0 for each element of Newtask do (which have the form {~,(cr,T,(Rl, ·.. , Rn))}) U2:=U2U{cr,T,V(Rl, ... , Rn)} return U2 else return INSORK(Newtask).