A Prover for General Inequalities

1. INTRODUCTION

This paper, which is an abridgement of [1], de­ scribes a program that has been used to prove a number of first-order theorems involving in­ equalities (and equalities). It is a variation of an earlier natural deduction prover [2]. The class of formulas dealt with permits arbi­ trary quantification and uninterpreted function symbols and can therefore encode predicate cal­ culus. Our intention, however, was not to pro­ vide a general-purpose prover for first-order logic but rather to be able to prove naturally arising formulas involving inequalities. We have made use, where possible, of previously developed techniques. Among these are decision procedures for ground Presburger formulas [3-8] and the restriction variable methods of [9]. We emphasize that this prover is completely automatic and that all examples were proved without recourse to human interaction. So far as we are aware, this prover is the first one able to prove formulas of the kind typified by the examples in an automatic way.

2. THE PRINCIPAL PARTS

Because of space limitations we are forced to refer the interested reader to [1] for the de­ scriptions of the algorithms that the program employs. However, we must mention that the heart of the program is the routine IMPLY, which coordinates the search for the proof of a theo­ rem. The guiding principle of this search is the retention of the implication symbol as the main connective of the theorem being proved.

Without going into detail we also note that when the conclusion of a theorem is an ine­ quality, IMPLY causes a function named PROVE-LE to be called. This function in turn calls several subfunctions:

1. LESS=

A quick routine designed to solve such trivial subgoals as 4 S 5, 6 < ~, etc.

2. PROVE-LE-GROUND-CASE

Called if the conclusion is a ground ine­ quality in an attempt to establish whether this inequality follows from ground inequalities in the hypothesis (stored in a special data struc­ ture called the TYPELIST) .

3. RESTRICTION-LE

Called if the conclusion is a non-ground in­ equality which can be "solved" by simply plac­ ing restrictions on variables which occur in it.

4. MATCH-IN-TYPELIST

Called when the conclusion is a non-ground inequality (which cannot be "solved" by RESTRICTION-LE) in an attempt to "solve" it by finding a match with a ground inequality stored on the TYPELIST.

5. MATCH-LE

Called if the conclusion is an inequality and none of the above techniques succeeds (or applies) in an attempt to use the hypotheses of the theorem other than those on the TYPELIST.

In the section of examples we use the following abbreviations for these functions:

GLE for PROVE-LE-GROUND-CASE

Data Base

A data base, DB, is employed which is "dynamic" or "contextual," in that it may change as the proof progresses. It has three parts: A-UNIT, RESTRICTION-LIST (or RL), and TYPELIST (or TY). The A-UNIT is not used here (see (9]).

RESTRICTION-LIST (or RL) is the place where re­ strictions on variables are recorded. If, for example, an entry

is present in RL, it means that the variable x (which is to be instantiated, or bound to a value) has not yet been given a definite value but has been restricted to reside in the inter­ val-;-< x <b. If later x is bound to a particular value c, then c must satisfy this same constraint, a < c < b. Other restrictions like a ~ x S b, a < x < b, etc. are possible.

TYPELIST (or TY) is the place where ground ine­ quality information is stored. If an entry

is present in TY it means that one of our hypo­ theses is a < x < b. Notice the fundamental difference b;twe;n this and (1) of RL. In RL, x is a variable to be instantiated, whereas in (2) it is a constant. RL represents knowledge about the "solution" to their variables (i.e., the bindings for the variables), whereas TY represents given knowledge or hypothesis knowl­ edge that can be used to obtain the solution. Getting a contradiction in TY is desirable in that it completes the proof of the current sub­ goal, whereas a contradiction in RL is undesir­ able in that it indicates a failure to find an acceptable solution (binding) for x. An entry like (1) represents a whole interval of accep­ table solutions for x (provided that it can be proved that a < b).

Other concepts such as REDUCTIONS, controlled backtracking, and algebraic simplification are used to advantage.

3. EXAMPLES

In the following examples we will depict a call to IMPLY as follows:

Here the theorem label, TL, a map for keeping track of subgoals, is in the left margin. The

RLE for RESTRICTION-LE MTY for MATCH-IN-TYPELIST MLE for MATCH-LE

TYPELIST, TY, being part of the hypothesis, is shown with H to the left of the arrow implying C. The restriction list, RL, is shown to the right. In the descriptions of proofs of the ex­ amples we will often leave out some of the steps when clarity is not impaired. Also, the compo­ nents TL, TY, H, c, and RL will not all be given at each step.

The theorem label, TL, starts as an empty list () and grows as the depth of the proof in­ creases. It consists of a sequence of symbols representing the actions that have been taken. Some of the symbols used in TL are

• 1 first branch of an and-split
• 2 second branch of an and-split

p...

promote

CHECK check that a proposed binding is consistent with RL

In the following examples all symbols a, b, c, f, g, £, etc. that are not explicitly quantified will be treated as skolem constants.

PROVE-LE is called, which calls LESS= and RLE, which fai 1.

PROVE-LE then calls the ground prover GLE which succeeds as follows:

The ~(b < £) = (£ S b) is inserted into TY which becomes

CONTRADICTION is called but it finds no contra­ diction in TY; however, it does find and return the equality unit (b = £), which is then applied to TY to obtain

which has a contradiction. Q.E.D.

Note: y is a variable, Zy is a skolem function of y, and the other letters represent constants,

LESS=, RLE, GLE, and MTY fail.

MLE: Zy ~ b: b/y

Note: The substitution b/y has succeeded on subgoal (P .... l); prover will not proceed to sub­ goal (P-+ 2) with y replaced by b,

GLE inserts - (b < £) into TY which becomes

<X>NTRADICTION discovers the equality (b = £) in TY, getting

which holds a contradiction. Q.E.D.

PROVE-LEis called which calls LESS= whichnnls, PROVE-LE then calls RLE which succeeds with

Here RLE has intersected the interval (x: a~ x < oo) with (x: 0 < x < 5) to obtain the desired result, Howev;r, before it can re­ turn this answer it must verify that it is not empty; i.e., that a~ 5.

PROVE-LE calls GLE, which inserts ~(a ~ 5) -

(5 < a) into TY to get

which has a contradiction (by routine CONTRADIC­ TION). Q.E.D.

The reader is referred to [1] for a description of the proofs, given by the prover, of Examples 4-6 below. LUB, Ll, and L2 are lemmas used in these proofs.

4. REMARKS

The authors would be interested in hearing how well other provers are able to handle these examples, especially Ex. 4-6.

One of the reasons for our success here was our use of devices such as an algebraic simplifier to avoid the explicit use of the axioms of the real number system. Our special handling of inequalities also attempted such a saving by avoiding such axioms as the transitivity of < _,

(x < y ~ y < z ~ x < z), but much more needs to be done if ;e are t~ smoothly and economically handle the "low level" calculations associated with proofs in analysis. For example, special techniques are needed for absolute values, especially when they occur in connection with inequalities.

We don't think of this prover as ultimate in any sense. At best it will become a part of a more powerful prover we are now trying to build, which will include many of the features men­ tioned in [10]. For instance, recent work in­ dicates that the use of automatically generated counterexamples can greatly speed up the proofs of these examples and others like them.

ACKNOWLEDGEMENT

This work was supported in part by National Science Foundation Grants MSC 77-20701 at The University of Texas at Austin and MCF 76-81425 at SRI International.