Using Examples to Generate Instantiations of Set Variables

W. W. Bledsoe Department of Mathematics and Computer Science The University of Texas at Austin Austin, Texas 78712, USA

ABSTRACT

Examples play a crucial role in automated theorem proving, not only as counterexamples to help prune unproductive subgoals, but also to help guide proof discovery. In this paper we show how examples (interpretations) might be used to help determine instantiations of set variables. We also discuss the role of piecewise-linear continuous functions, and give some results of computer runs using these methods.

I INTRODUCTION

This is part of an e ffort to use examples (interpretations) to help in automatic proof dis­ covery [1). We believe that examples are not only useful as "counterexample sleves", to prune the proof-search tree, but also can be used to help guide the search. One way this is done, is in finding instantiations of variables . See [1, Section 2). Here we show how examples might be used to help instantiate set variables.

One reason that examples are so valuable in theorem proving is that they allow us to calcu­ late, as opposed to prove. And since calculating is usually easier than proving, this gives an advantage. But of course the results from examples are less general, so the attack has to be balanced - with some calculation and some proving.

Let us start with the following problem: Given a continuous function f on [a,b), with maximum value at x = £ .

To find a subset A of [a,b) for which £ = sup A. Describe A in general terms, in terms of f, a, b. E. g.'

We desire to generate such an A auto­ matically. How? Why? Motivation for this ex­ ample: If we wish to prove the theorem that interval, attains its maximum on that interval,"

using the least upper bound axiom

LUB "Every non-empty, bounded, set A has a least upper bound, sup A",

then we must have a value of tion of A in terms of f, a, utilize LUB in the proof. A (i.e., a descrip­ b), before we can

Once A has been given, the theorem will have been reduced to a theorem in first order logic about general inequalities.

More generally, when we are trying to prove a theorem of the form

using the LUB axiom to produce a set A f or which £ = sup A, then (1) can be written

which is equivalent to

E.g.'

e.g.'

If we further assume that for each f sat­ isfying H(f), there is a largest t in [a,b] for which (1) holds, then (3) is equivalent to

So our objective is to prove

This has the general form

So for this form of theorems our problem is:

Given H and 1)! ·

Generate Q for which (5) holds. How? We pro­ pose to do this (automatically) by using inter­ pretations (examples) f of f (and interpre­ tations of the other function and predicate symbols appearing in H and lj!).

We will first state our problem in a more general setting and then (in Section 4) return to the forms (5) and (4) as special cases.

II GENERATING PREDICATES

Suppose that P is a list of uninterpreted function symbols and predicate symbols (which does not contain the symbol Q). Let L = { 1\ ,v, -,+, V, 3 ,5, <,=}, LE = {:s; <}, and let H and 1)! be functions over the symbols of P U L U {Q}. By an interpretation of P we mean a list of inter­ pretations of its members. For example, ~f ~ is {a,b,t,f} , then P is {a,b,~,f} , where a, b, ~. f, could be~= 0, b = 1, ~ = 1/2, f ='Ax(2x- 1), for example.

Now suppose that we are to prove a theorem of the form

The object then is to find (generate) a Q which satisfies (6).

We propose the following general method for finding Q.

• (i) Obtain an interpretation fr of P which satisfied H(P).
• (ii) Generate a predicate Q, in terms of P, which satisfies

• (iii) Test Q on other P's.
• (iv) Prove (6) using the Q so obtained.

Of course, finding Q is equivalent to proving a theorem in higher order logic, which requires the higher order variable Q to be instantiated. The central idea is this: if a Q can be found which satisfies 1)!\P,Q) for P's (which satisfy H(P)), then hopefully that Q will also satisfy lj!(P,Q). We will indeed see that that is the case for some special instances given in Section 4 below.

We will defer discussion of Step (i), the fabrication of P, until Section 3 (a subroutine, INSTANTIATIONS, does this), and concentrate now on (ii), the generation of Q for which 1)!(P,Q) holds. Step (iii) is rather straightforward, and Step (iv) is not within the scope of this paper*.

So let there be given an interpretation P satisfying H(P). We desire an algorithm GENERATE which will generate a Q satisfying lj!(P,Q). Of course ~uch a Q may not be unique (even for a fixed P.

If the algorithm GENERATE is indeed to gen­ erate such a Q, then it must use an association between the members of P and those of P. Because, Q is to be given in terms of the symbols in P, not p, and it must satisfy the condition 1)!(P,Q) where every p in p has been replaced by an interpre­ tation P.

It is not obvious how to build such an algo­ rithm GENERATE, but somehow it should key on the structure of lj!. The following, GENERATE, is a first attempt at such an algorithm. It is built on several additional assumptions, given below, about P and lj!. (The symbol "Q": in the following algorithms will ~ represent the predicate we are looking for- i.e., trying to generate.)

*It is often the case, as in the examples of Section 4, that once an instantiation Q of Q has been given, the resulting theorem VP[H(P)-+lj!(P,Q)] is first order. And while it still may not be easy to prove it, nevertheless, lends itself to standard procedures.

We will assume that complete ~* informa­ tion is available on lj!, Q, and members of P. Thus, for example, Q might be a predicate over the reals, so that for each x £ R, Q(x) is either

true or false. (E.g,, Q(x) = f(x) ~ 0).

For our first version we will assume that Q is a function of ~ real variable x. (In general

we might restrict Q to a function on Rn.)

We will start with a call to

" with n;l, and where B ; P x P and 'x is the argument of Q. B is treated as a set of bindings, tying members of P to those of P. (I.e., B is a substitution). B will be expanded as new vari­ ables and their instantiations are added. If A is a formula then AB is used to denote the result of applying the substitution B to A.

The integer n is the number of variables used in the description of Q. If n;l, then Q is expressed only in terms of x, e.g., 0 ~ f(x); if n;2 then Q is expressed in terms of x and y, e.g., Vy £ [a,x) f(y) ~ f(x); etc. (Note: The parameter n counts both bound and free variables.)

The first call to GENERATE is made with n;l. If this fails (returns NIL), then n is increased by 1 and a new call made to GENERATE, etc., up

to a maximum allowable value for n.

(Before presenting the algorithms GENERATE, TALLY and ALL-SOME, let us try to help the reader by pointing out that we are looking for statements that can be deduced from a given example, function f, that might hold for the whole interval [a,b] or for a part of it; that the method works by looking at the critical points of the example function; that GENERATE, TALLY, and ALL-SOME, return families of conditions that are true on the subintervals; that these families of conditions are combined in appropriate ways to give candidates for the Q that we are looking for; and finally that this combining action is governed by the structure of the formula ljJ containing Q.)

The objective is to find a Q for which ljJ(P,Q) PIP is true. x is a variable. It starts as 'x,

the argument of Q.

Form of ljJ ACTION

1. 1/Jl A \jJ2

*See, for example, Peter B. Andrews, "Resolution in Type Theory", J. Sym. Logic 36 (1971), 414432, [5].

(Each of Q 1 and Q 2 is a set of formulas).

Note: alternatively verify it in itinlj! 1 ). we might generate Q 1 and lJ! 2 (or generate Q 2 and-verify

1. lj!l v lj!2

3. Vx' £ [a,b]*P(x' ,Q)

Select randomly~ points x 1 , ··· ,xk from [a,b], including the endpoints.

4. 3x' £ [a,b]*P(x' ,Q)

Select randoml~ points x 1 , ··· , xk from [a,b], including the endpoints.

Return Q 1 U Q 2 U ·.. U Qk

*Similarly for open and half open intervals (a,b), [a,b), (a,b]. In these cases the open endpoints are not selected for x, but "nearby" points are

selected (see Section 3.5).

tThe number k used here is a parameter supplied by the user. See Section 3.5 below for an alter­ nate way of selecting the xi when f is a piece­

wise linear continuous function.

5.

6. Return -Q'* Q(~)** Put B = B u {(x,x)} x-list = {x}, ~-list = {~} If n = 1, return TALLY (B, x-list, ~-list, x) Else return ALL-SOME(n, B, x-list, ~-list, ~) TALLY (8, x-list, ~-list, ~')

Pis a set of predicate and function symbols, fJ is a set of interpretations for members of P, x-list is a set of variables (e.g., {x,y,z}), ~~list is a set of real numbers, instantiations for x-list,

B is a set of bindings: B = (P x P) U (x-list x ~-list), x' is a variable, the last element of x-list.

This routine is supposed to determine "what is true" about p u x-list (for x' only) and record that information in terms of P U x-list.

(NOTE: This is similar to the conjecturing of Lenat [2). See Section 4 below.)

Let H1 be the first and second level terms of P U x-list (i.e., constants, variables, and one­ level application of function symbols to these (part of the Herbrand Universe)). (In later ver­ sions we might try to use second-level applica­ tions, etc.)

Let A be the atoms associated with P, LE, and H 1 , but only those containing x'.

Let S be the set of all atoms A of A for which AB is true, and for which A is not a tautology.

Return S. (Treated as a conjunction.) (Note: S might be NIL).

AB is defined to be the result of replacing any member of P U x-list in A by the corres­ ponding value P U ~-list.

The following is an example of the use of TALLY:

*Since Q' is a list, the list of negations of its members is returned.

**Recall that x is a real number in [~,b). By the time that step 6 is applied, all variables will have values.

Remark. The list S might be rather large unless additional restrictions are placed on H. So in TALLY, it is convenient (for eff iciency purposes) to have further "typing" information which, hope­ fully can be derived automatically from the theorem being proved. For example, in proving the theorem:

we note that: a, b, 0, x, f(z), f(b), f(x) all have type Real. But in the context of this theorem this set can be partitioned into two sub­ sets

So in TALLY we should not build atoms of the form x ~ O, a ~ 0, but only-rhose of the form f(a) ~ O, f(x) ~ 0, etc. Such additional know­ ledge was used in the above example and in those of Section 4. This concept requires much further study.

This routine will not be used unless n ~ 0. If n = 2 it will introduce a new variable y, and give it some values Yl· ··· , Yk in [~, xo), and Yi ···· , Yk in (x 0 ,SJ, and tally "what is true" about each of these Yi's and yi's, (in terms of P, x-list), and finally deduce statements of the form Vy E [a,x) P(y), ]y E (x,b) P(y), etc., and return these. If n > 2, then yet another variable 'z is introduced (for each Yi· yi), n is decreased by 1, etc.).

*We show here only the case n = 2. For n ~ 3, the procedure is appropriately generalized to handle intervalsAo~ the fo~ (x0 ,yi), (yi,x0), etc., as well as [a,x 0 ) and (x 0 ,S). Also See comment below.

2. For each i, put

(NOTE~ y is a new variable symbol).

1. If n = 2' put

Else put

1. Put

s. Return QQ U QQ'

Comment. We have arbitrarily restricted the new variable 'y (see 1. above) to the intervals [a,x 0 ) and (x 0 ,b). This might be too restrictive. Perhaps we should have also considered y's in the intervals, <~ .· ~ 0 ) for each x. in x-list, or other possibilities~ J

In the case n = 3, the predicate Q will be described in terms of three variables x, y, z. In this case, after the Yi have been selected as in­ dicated in Step 1, another call to ALL-SOME will cause (by Step 1) points z 1 , ··· , zk to be se­ l~cted from each of the intervals [a,x0), (x0 ,SJ, (x 0 ,yi), (yi,x 0 ), i = l,k. Similarly when n ~ 4.

This is used by ALL-SOME.

Here S is a set

where each Si is a result from TALLY. The Si are treated as sets rather than conjunctions,

and etc.

and for each ~ £ aS, let

and return the conjunction of the members of the set

(This might be NIL).

The Algorithm COMBINE-ALL-S as defined here produces the simplest answer from a set S, as de­ picted by the following examples.

where A, B, C, D are some f ormulas

COMBINE-ALL-S returns

But in EX 3 (and similarly in EX 2) it could have returned the correct but more complicated answer

Our implementation of COMBINE-ALL-S allows both options; the simpler version produces more tractable answers for instantiation of set vari­ ables (see IMV and AMlin Section 4), but the more complicated version was needed for EX 5 of Section 4.

III Obtaining Interpretations P

The fabrication of an interpretation P of P which satisfies H(P) for a given H, is itself a challenging problem. In general it cannot be handled automatically.

It is not the main purpose of this paper to discuss the problem of fabricating these ~'s but in using them. However, we do have some sugges­ tions.

A. Human Supplied Interpretations

One possibility is that the user supplies the P's, either at run time, or in a convenient know­ ledge base which the program can effectively access. See, for example, [3]. Such a collection of ex­ amples could accumulate over a period of time and be used for a number of applications. In the ex­ amples of Section 4, we show the obtaining of the needed interpretations by a call to a subroutine INTERPRETATIONS.

B. Piecewise-linear continuous functions

For the special case when the examples needed are interpretations of continuous functions on a closed intervc,l of the real line, we might employ piecewise-linear continuous functions (pelf's) in a number of applications.

These have the advantage that are easy to generate and use. Such an f with n corners, can be gen­ erated for the interval [a,b], by generating n random numbers x 1 ,x 2 , ··· ,xn in the interval [a,b],

(sorted), and n + 2 random numbers ya,y 1 , ··· ,yn,yb' and putting

Such plcf's were used in the examples of Section 4.

A If one needs a plcf f which satisfies an additional constraint H(f), then one can either: generate f's and test them until one satisfying H(f) is found; or try to build into the generating routine the ability to restrict such f's. Again this second approach appears to be difficult in general, though we were able to realize it for special cases such as:

or

It might also be useful to build up a special set of routines for handling pfcf's, for evaluating ~ at specific x's (numbers), and for computing their maximum, minimum, zeros, etc.

C. Infinite Number of Corners

If a plcf with an infinite number of corners is needed, then one might use a formula for com­ puting the x and yn instead of the list of number pairs.n For example,

represents the plcf

In working with such a plcf, the computer would deal with this formula instead of with a list of pairs of numbers.

In addition to such a description, one might want to add a finite number of fixed points (e.g., (0,0)).

D. Piecewise-linear Functions With "knees"

If the interpretation f of f is required to be differentiable as well as continuous, we might want to place quadratic "knees" on our plcf' s, or "cubic" knees if the derivative of f is re­ quired to be continuous, etc. Again one would need to develop a set of routines for evaluating f at particular x's, and for finding maxima, minima, zero's , etc., for such f's.

We do not recommend that polynomials be used as f's because in order to obtain an example with a few undulations, it is necessary to use a poly­ nomial of order four or higher, and these are very difficult to compute.

E. Using the "Corners" of f

plcf's have another advantage besides being easy to compute. For example, if we are trying to tally the formula (f(x) < f(.499)) for values of x within the interval I 1 , the program could just as well use the corner points of f, that is only x's for which (x,y) E f. Thus in the algorithm GENERATE, Steps 3 and 4, where random points, xl, ····Xu· are selected, we might instead have used for the xi's, the x's corresponding to the corners of f. / ', A

I.e., we need only check f(x) ~ f(.499) for x equal to the values x 1 ,x 2 , ··· ,x 6 ·

However, if we are using two variables x and y in the description of Q (see algorithm ALL­ SOME, Section 3), and are trying to tally the formula (f(y) < f(x)) for x in interval I1 and y in Interval Iz, it is also necessary* to con­ sider additional x:s and y's corresponding** to the corner points of f.

Thus x is allowed to take the values xl,xz, ·.· , xlO· which lie within I1 and once x is given such a value, x, y is also allowed to take these values xl·····Xn (within Iz) as well as other values "close to" x (see Section 3.6) and points corre­ sponding to them. Of course, this lacks generality but can be shown to be adequate in certain theorems about inequalities. For instance, it was success­ fully used in the examples of Section 4.

*Necessary because these give all the points at which simple inequalities might change truth values.

**We say a point x' corresponds to a point x" (with respect to f) if f(x') = t(x").

F. Choosing Points From Open Intervals

In algorithms GENERATE-1 and ALL-SOME we often are required to select points x1 , ··· ,xn (or Yi's or y''s) from open and half open intervals as well as ciosed intervals, so we cannot always automatically include the endpolnts. In these cases we have used a parameter E (small) to pick points "clo~e" to the endpoints. For example, from the interval (a,b) we would select (among others) the point a + E. The parameter E is allowed to diminish in value by multiplying it by 1/10 each time it is used. For an open interval (c,d) we have / "A Jf X "f X

.

In this example theApoints x 2 , x 3 , x 4 , are selected at the corners of f, while x 1 = c + E, x 5 = d - E, for the open interval ( c ,d).

Using the example of the previous section (3.5), if I 1 is (l/2,b), and I 2 is [a,x), then x would be allowed to take the values x4 + E , x 8 , x9 , x5, xlO· x6. And onc.e x is given the value x 8 , then y is allowed to take the values x 1 , x 2 , x 3 ,

\le consider two theorems IMV and AMl, and · show (partially) how GENERATE works on them. See [9) for further details and three other examples. (These examples were all done by a computer program; however, the program is not considered optimal or final at this time.)

• IMV (The intermediate value theorem): If f is a continuous function on the non-empty, closed, interval [a,b), f(a) ~ 0, f(b) ~ 0, then for some x in [a,b), f(x) = 0,
• AMl Each continuous function f on a closed in­ terval, attains in maximum (minimum) on that interval,

using the least upper bound axiom

• LUB Every non-empty, bounded from above set A has a least upper bound, sup A.

In symbols we have

• IMV LUB A f is continuous on [a,b) A a ~ b Af(a) ~ O, A 0 i: f(b)

AMl LUB A f is continuous on [a,b] A a ~ b -+ 3 £ E [a,b] Vx E [a,b] (f(x) ~ f( £)),

where,

Our obj ective in each of IMV and AMl, is t o instantiate the set variable A of the hypothesis LUB, and thereby reduce both IMV and AMl to theorem£ in first order logic .

Notice that they both have the form (1), p. 4, where for IMV, H(f) is

LUB A continuous f[a,b] 1\ f(a) ~ 0 A 0 ~ f(b)

and f or AMl, H(f) is

and following the steps described on pages 4-6 we obtain formula (4), p. 6, with

for IMV, and

for AMl.

Example 1 (IMV)

a call to INTERPRETATIONS yields ~ = O, b = 1 f {(0- .2)(.2.2)(.3-.4)(1 1) }. ~·

1

A call to CALCULATE-L yields £ = 1/2. (In the spirit of the "calculate vs. prove" remarks in Sec­ tion 1, we of course call on the program to calcu­ late a valueAof £ satisfying the theorem (for a particular f)).

*We have chosen to represent f(x) = 0 as f(x) ~ 0 AO ~ f(x), which is required by our present pro­ gram. It is not at all clear whether we can easily change the program to handle this example other­ wise.

For these values of a, b, f and £ , the formula ( 7) reduces to

A call is made to �ENERATE-1(~). (We suppress the arguments n, S, and 'x) which (by Rule 1 of GENERATE) recalls itself on ~l and ~2. GENERATE

By Rule 3, the points £i·····£4 are selected as £i = 0, £2 = .2, £) = .3, £4 = .499*, and calls are made to

and each of these, by Rule 4, select points x1 , ··· , xn from (£i,l/2) and calls GENERATE(Q(xi)) which in turn calls TALLY.

For example, when £' takes the various values shown below, the corresponding values of x 1 , ··· ,xn are chosen and calls to GENERATE(Q(xi) and TALLY yield the results shown.

Then from Rule 4 of GENERATE, we obtain the union of these various subgroups for (8), (9), (10), and (11). I.e., {f(x) < 0, 0 < f(x)} is re­ turned from (8); {f(x) < 0, 0 < f(x)} is returned from (9); {f(x) < O} is returned from (10); {f(x) < O} is returned from (11).

These are intersected (by Rule 3 of GENERATE) to obtain {f(x) < 0}.

Recapitulating from (7'): a call was made to �ENERATE(~l) which yielded {f(x) < 0}.

Next a call is made to �ENERATE(~ 2 ) �ENERATE(~ 3x E (1/2,1] Q(x)). By Rule 5, it calls first GENERATE( 3x E (1/2,1] Q(x)), which yields {0 < f(x)} and this is negated to obtain {f(x) ~ O}. Then by Rule 1, {f(x) <O} and {f(x) ~ 0} are "interse.£ted" to obtain {f(x) < O} as the final answer. (In intersecting these, {f(x) <l _O} is treated as {f(x) < 0, f(x) = 0}).

*We are using the "corners" method described in Section 3.5.

This answer, {f(x) $ O}, is checked ag~inst other values of t, and, finally the set A in Theorem IMV is given the value

which is a correct instantiation.

Incidently, when A is instantiated with this value (14), the theorem IMV is reduced to the first order theorem:

Of course we would need to add the definition of continuity and, unless one uses a general in­ equality prover like [4], also add the axioms for the densely ordered reals.

Example 2. (AMl) ·

A call t o INTERPRETATIONS yields ~ = 0 , £ = 1, ~ = {(0 0) (.1 .2) (.3 -.2)(.5 .5) (. 7 -.3) (.9 .3) (1 0)}

a call to CALCULATE-L yields ~ = 1/2.

As in Example 1 we obtain (exactly) the formula (7'), and calls are then made successively to �ENERATE(~), �ENERATE(~ 1 ), �ENERATE(~ 2 ), which return the lists, {\t'y E [a,x)(f(y) < f(x)), ]y E (x,b](f(x) < f(y)), 3y E (x,b](f(y) < f(x))}, and {\t'y E [a,x)(f(y) .$ f(x)) }, which are inter­ sected to obtain {Vy E [a,x)(f(y) < f(x))} which is returned by the call �ENERATE(~) .

Let us now examine in more detai l the call, �ENERATE(~ 1 ), i.e.,

Rules 3 and 4 are used to select CR-i····· R-4) equal to (0, .1, . 3, . 499), and for each R.', x 1 ··· x as shown below. We show here some of the'cor;e~ spending output from GENERATE. (See [9] for fur­ ther details.)

In the following table

If one of these is primed, then .$ is used instead of <.

These are now intersected to yield

from (15). �ENERATE(~ 1 ).

The call �ENERATE(~ 2 ),

causes (by Rule 5) a call first made to GENERATE­ ( 3x E (1/2 ,1) Q(x)), whose result i s negated and returned for (17).

Rule 3 is used to select (.5001 .7 . 9 1. ) for (xl x2 x3 x4), and GENERATE)Q(xi)) is called for each to obtain the results shown below.

The union of these {SOME 1 SOME 2 ALL 2 ALL 3 ALL4} is then returned, and this is negated to yield

from call (17). Finally, (16) and (18) are inter­ sected to yield {ALL].}= {7 y E [a,x) f(y) < f(x)} from the call �ENERATE(~) .

This is checked against other values of f, and finally, the set A in Theorem AMl is given the value

See [9) for further details and three other examples.

V Comments

A. Higher Order Logic

Since instantiating set variables is a part of higher order logic, one could also use proce­ dures like those of Andrews [5), Huet [6), Darlington [7), or possibly Bledsoe [8). In gen­ eral we would expect these to be less efficient than the technique discussed here, but further experience is needed.

B. Conjecturing

The central component of this work is the routine GENERATE which attempts to general (des­ cribe) a predicate Q(x) satisfying a particular form ~(Q(x)). This is much in the spirit of Lenat's work [2), where various conjectures are derived from examples.

In Lenat's work as well as ours, there is given a set of examples and the program is asked to determine "what is true" about them. There is a difference however: whereas Lenat asks all that is true (about his examples), we ask what~ specifically true about certain objects in P, such as f.

Such conjecturing seems to play an important role in all of human endeavor, and we would expect a prominant place for it in future automatic reasoning systems.

C. Calculate vs. Prove

We cannot over emphasize the importance of being~able to calculate properties about a partic­ ular f rather than prove the same properties about the uninstantiated variable f .

For example, for the continuous function, f Ax (4x - 4x2), it is rather easy to auto­ matically calculate that ~ = 1/2 is the maximum of f on the interval [a,b] = [0,1]. However, it is indeed difficult to prove automatically that any continuous function of [a,b], with as b, attains its maximum on that interval.

D. Other Example Theorems

We hope to extend these results to other example theorems such as: Heine-Borel Theorem Nestled Interval Theorem, Baire Category Theor~m, Balzano-Weierstrass Theorem, etc.

In many of these one will work with families of sets (intervals) instead of functions. There is a natural analogy between piecewise-wise linear continuous functions (plcf's) and finite families of intervals. Accordingly we would expect instan­ tiations which consist of a finite family of inter­ vals, to suffice for many applications. But infi­ nite families will also be needed. See [9).