A New Mehtod for Proving Certain Presburger Formules

1. Introduction

Presburger Arithmetic.

An expression is said to be a formula in Presburger arithmetic if it is a (well) formed algebraic expression, allowing only variables, integer constants, addition and subtraction, the arithmetic relations ~ and ~, the propositional calculus logical connectives, and quantification (either universal or existential). Constant multiplication is also allowed. See [3), Davis [2), and Cooper [1).

The Presburger algorithm is a decision pro­ cedure for Presburger arithmetic: Given a form­ ula in Presburger arithmetic decide whether it is true or false. Two main steps are utilized in this process: (i) Elimination of quantifiers (and replacement of variables by constants) (ii) Evaluation of the resulting formula (which has no variables) to determine its validity.

Cooper's method.

Cooper [1) utilizes such a procedure. For example his method would convert the theorem 'ix(x < 1 + x < 2) successively to

[2 < 1 /1 1 < 2), which is easily verified as true.

Apparently Cooper's method can result in a search through a list of consecutive integers when the coefficients of x are not unity. For example, the theorem 'Y/ x (5x < 11 + 7x < 16) is converted to - :I x (5x < 11 /1 15 < 7x), and

which requires testing the expression for each of the integers, j = 1, 2, ... , 35. In fairness to Cooper it should be stated here that such adverse examples apparently do not arise often in the applications he considers in [1].

Our method, and in more detail in [8), Presburger arithmetic has many applications in the field of proving assertions about computer programs. There a theorem about the program, is required to be proved. Such theorems are often not originally stated as formulas in Presburger Arithmetic but are reduced to such as the proof proceeds. For example for an array A, we might be given the theorem: V j(j ~ 4 /1 'tt/k(k ~ 5 +A[k) < A[k+l)) + A[j] < A[j+l]).

- Backchaining ;n the second hypothesis gen­ erates the subgoal (j < 4 + j < 5) which is a formula in Presburger A;ithmetic. Notice that j is a universally quantified variable or free variable and hence must be treated as a skolem

1 constant in the proof. Many applications result in Presburger formulas with only universally quantified variables. In this paper we describe a procedure, the sup-inf method, for deciding the validity of such formulas.

First let us note that the above formula (j ~ 4 + j ~ 5) is easily verified by 1 adding the negation of the conclusion to the hypothesis, getting (j < 4 /1 6 < j) and then combining to get the cont;adictio~ (6 ~ j ~ 4). Our pro­ cedure does essentially the same thing on this example. We now describe in Section 2 our pro­ cedure for determining the validity of univer­ sally quantified Presburger formulas. In Section 3 we define the pivotal algorithms SUP and INF and prove in Section 4 of [8] that they terminate with desirable outputs when applied to quasi-linear formulas. Several examples are listed in Section 3, and given in more detail in Section 5 of [8). This method has been pro­ grammed and used extensively in a program veri­ fication system [6).

2. The Sup-Inf Procedure

An Example using the procedure.

We begin with an example and the general procedure. then outline

Let F be the theorem

Notice that F has 3 (universally quantified)

1 The skolemization process will not be discussed here. These universally quantified variables (or skolem constants) will be referred to as "variables" in this paper.

variables x 1 ,x 2 ,x 3 . We will negate F and con­ vert it to the expression (8') below, which gives a range for each of these three xi's. (Ex-

pressions (5'), (7'), and (8') correspond to ex­ pressions (5), (7), and (8) given later in our general procedure).

We first obtain

as the negation of F, and then convert it to

and finally to

To show the invalidity of (8') we calculate a lower bound ~l for x 1 and an_ upper bound x 1 , and check that the interval [x 1 ,x ] contains no integer. For this example, x- = h and x - 5 s 11 -1 T 1-3' and since 3 < 5i we are finished. ~l and x 1 are computed by the algorithms INF and SUP given in Section 3.

Quasi-Linear Formulas.

The reader will observe that expression (8') is not a Presburger formula because it conS 5 3 tains non-integer constants <3, 2, 2, etc.), and the symbol "min". We now relax the condition on the integer constants to allow ~ rational number as well as oo and - ou . However, the variables (such as x 1 , x 2 , x 3 in the above example) will represent only non-negative integers. We also allow the symbols "max" and "min" . Such an ex­ tended Presburger formula will be called quasi­ ~· It will be called "quasi-linear in L" if each of its variables is a member of the set L.

We now describe our general procedure for determining the validity of such quasi-linear formulas.

Let F be a quasi-linear formula in the variables x 1 , x 2 , .. . ,xn . We first want to convert - F to the disjunctive form

3 (F 1 V F 2 v .. . v Fp) where each of the Fi is a conjunction of the form

2 How 3 ~ 2x 2 -1 is derived from 2x 2 { 3 is ex-

plained in Section 3 of [8] .

3 In our example above we had only one F . This has been the case in most examples we ~ave tried

so far.

and each aj' b j are quasi-linear expressions the other xk (but not in xj). This is done follows: in as

The Sup-Inf Procedure . First, place -F in disjunctive normal form (G 1 V G 2 v ... v Gp) where each Gi is a disjunct of the form

and the Ai, Bi, Ci, Di are quasi-linear ex­ pressions in x 1 , x 2 , ... ,xn. We eliminate the equalities in (4) by converting each (Ci"' Di) into (Ci ~ Di 1\ Di ~ Ci) 4 so that each Gi has the form

Now each (Ai ~ Bi) is converted into a set of exactly n inequalities

by "solving for" 5 each of the xj occuring in Ai and Bi in terms of the other ~· Thus the aij and bij appearing in (6) are expressions in the other ~ (but not xj). If xj does not occur in Ai or B i then we put aij = 0, b ij = -T-. So (5) is converted to

(a 1 ~ x 1 ~ b 1 ) /\ .. . 1\ (a < x < b ) n- n- n '

where, for k = 1, n, ~ = (max a 1 k a 2 k . .. amk) 6 bk = (min blk b 2 k · · · bmk). Thus, by this whole process we convert - F to a disjunct

4 In practice we do not always convert the equalities to inequalities, but rather use a "substi­ tution of equals" technique to gain efficiency .

See [9).

5 In solving for x 1 in an expression like sup (x 1 + 2, x 1 ) ~ x 3 , we obtain two answers: x 1 ~ x 3 -2 and x 1 ~ x 3 instead of one, as indicated in formula (6). However, this presents no diffi­ culty in proceeding to (7) and (8).

6 The function MAX (See Sect . 3) is applied to the aik' If the maximum is not immediately attain-

able then the symbol "max" is employed. Simi­ larly for MIN. See for example, (7') and (8')

above .

where each FL has the form

and the ~k' bLk are quasi-linear expressions in the

Now we determine that F is valid by show­ ing that each FL is false.

Since the ~k and bLk are usually ex­ pressions in the other xi (as was the case in our example) it is not immediately obvious how one can test for the invalidity of (9). Our method (the "sup-inf'' method) for doing this is simply to test whether the interval

contains no integer, for some where sups ~ and infs ~ follows: k, k=l,2, ... ,n, are defined as

De fini tiona .

If S is a set of inequalities of the form (9) and xi, xi, ... ,x~ are real numbers, then (xi, xi, ... ,x~) is said to satisfy S if each inequality in S becomes true when each symbol ~ is replaced by the number xk·

If A is a quasi-linear expression in d ' ' ' 1 x 1 , x 2 , ... ,xn' an x 1 , x 2 , .·. ,xn are rea numbers then

denotes the number gotten from each symbol ~ by the number A by replacing xk·

If A is a quasi-linear expression in x 1 , x 2 , ... ,xn' then sups A is defined to be the least upper bound of all numbers

where (xi, xi, . ·. ,x~) is a sequence of non­ negative integers satisfying S. Similarly, infs A is the greatest lower bound of such numbers. When no confusion will arise we omit the subscript S and write sup A and inf A.

Thus the validity of F has been reduced to determining sups ~ and infs xk, where S is the set of conjuncts of (9). We compute sups ~ and infs ~ by the algorithms SUP and INF given in Section 3.

In Section 4 of [8) we prove that if S is ~ set of inequalities of the form (9) where we assume only that the ~i' bLi are quasi-linear in x 1 , .·. ,xn' then the outputs SUP(~,NIL) and INF(~,NIL) are numbers (or possible ± oo ) with the property

7 Furthermore, we conjecture there that if the set S is in "natural form", in that it has been derived from a theorem F by the procedure des­ cribed above, then equality hold in the above formula, i.e.,

Thus to show the validity of F we need only show that the interval

contains no integer for some k, k = 1, 2, .·. , n.

Some Discussion of the Procedure.

This procedure for deciding the validity of a quasi-linear formula (and hence for a univer­ sally quantified Presburger formula) is called the .!.!!2_-.!!t[ ~· Of course it serves much the same purpose as the methods of Cooper in [1) and others. However, we feel that the sup-inf method has some advantages, especially for proving theorems arising from program validation.

One such advantage is that a hypothesis, such as

from our earlier example (3), can be stored in the concise form

to be used to establish various conclusions as required. Thus if we desire to establish (2x 2 $_ 3) we need only update (10) with its negation (3 $_ 2x 2 -l) to get (8 1 ) and then show that (8') is invalid. Also, using this same hypothesis (10) we might (later) be required to prove another conclusion, which itself has a hypothesis, such as

In this case getting is used to update (8')

which is used to prove x 3 $_ 8.

Also as mentioned earlier it avoids proof by searches through long lists of integers.

While these arguments have merit, they are not our main reason for prefering the sup-inf method, which is our desire to efficiently handle certain "proof by cases." This is explained in [8, pp . 11-15], and in [7].

7 This conjecture has recently been proved correct by Shotak [ 10).

3 . Algorithms

Here we describe the pivotal algorithms SUP and INF .

If A and B are quasi-linear expressions in L (see definition in Section 1), then so also are (A+B), max(A,B), min(A,B), and r*A, where r is a rational number. We can also divide a quasi-linear expression A by a non­ zero rational number r by multiplying by its inverse, i .e . , 1/r * A.

Let S be a set of inequalities of the form a ~ xj ~ b where a and b are quasilinear in x 1 , . . . ,xj-l' xj+l' . . . ,xn . Recall the definitions of sups xj and infs xj given in Section 2 . We now give algorithms for computing sups xj and inf 5 xj for a given S. S will be assumed to be fixed throughout the remainder of this section .

Definition. MAX(x,y) is a function which returns y if x < y, x if y < x, and ("max" x y) otherwise- . Similarly for MIN(x,y) . If J is a variable, then S contains one (and only one) inequality of the form a < J < b, which repre­ sents knowledge about J. -If -a = 0 and b = +"' then nothing is stated about J except that it represents a non-negative integer . ·

The notation LOWER(S,J) and UPPER(S,J) is used to denote these lower and upper bounds on J. For example, if (2 < j < 3-K) is in S, then LOWER(S,J) is 2, and UPPER(S,J) is 3-K.

SIMP is an algorithm that puts expressions in canonical form . See [8,7] . All outputs from the algorithms SUP, SUPP, INF, INFF, are auto­ matically simplified by applying the algorithms S IMP to them.

SUP and INF .

SUP and INF are each called with two arguments, J and L. J is an expression and L is a list. SUP(INF) attempts to find the largest (smallest) value that J can have con­ sistent with the inequalities in S. (See defi­ nitions of sups ~ and infs ~ in Section 2) .

L is a set of variables. The first call to (or to INF) is usually given with NIL for variables are then sometimes added to L by cursive calls to SUP and INF. See Tables SUP L; re­ I, II .

SUPP and INFF.

SUPP and INFF are called with arguments x and y. x is a variable and y is an expression . SUPP is called by SUP when J is a variable and J i L. Similarly INFF is called by INF . StiPP is designed to handle the case when SUP(J,L) returns an answer which contains J itself . See Tables III, IV. - ---

The action of SUP can be viewed as putting together a string of inequalities . For example, if S consists of the inequalities [(0 ~ J < k) A (0 < k < 3) I then SUP(J,NIL ) will determine (J ....: k ...: J), and r et urn 3 as the correct value . How; ver; i f S cons i st s of I (0 , J < k) A (0 ::: k :... 6- .1) I then il Re t s (J :;;: k S 6-J) and it must solve this inequality to determine: (2J < 6), (J < 3) , and again return the correct valu; 3 . This type of "solving" is done by the algorithm SUPP. That is, SUPP (and analogously INFF) handles the cases when SUP(J,L) might re­ turn an expression containing J it~elf .

For instance, in the above example, where S consists of I (0 < J < k) ~ (0 < k ~ 6-J)], since J is a variable and J t NIL, -the al­ gorithm SUP (Step 2. 2) finds the member (0 < J < k) of S with J as its middle term, and-then puts Z: = (SUP k (J}). Since SUP (k, ( J}) (eventually) returns the value (6-J), a call is made to SUPP(J, (6-J)) which returns the correct value 3. In evaluating SUPP(J, (6-J)), SUPP expresses (6-J) in the form b J + c, with b = - 1, c = 6, and returns the

On the other hand if S had consisted of [(0 < J < k) A (0 < k < 6+J)], then SUPP would have been called-with arguments J and (6 + J) which would lead to b = 1, c = 6, and result in the correct value + .x. for SUP(J,NIL). That this is the correct answer can be seen as follows: From S we get (J < k < 6+J), which implies 0 < 6 . But this is n~ restriction at all on J, -and hence ·sups J = + ''· .

Examples.

In Section 5 of [8], Tables I-IV and the sup-inf method, are used to prove (or disprove) Examples 1-4 below, and to compute the indicated values of SUP and INF given in Examples 5-9 below.

• 1 . (x < 1 + x < 2)
• (5x < 11 + 7x < 16)
• (Sx < 16 + 7x < 16) FALSE
• 4 . (2y + 3 ~ Sz A z ~ x- y A 3x ~ 5 + 2y ~ 3)
• S = ((j: 0 k)(k: 0 j +L)(L: 0 2-j}) supS k = 2 = SUP(k,NIL)
• S = ((j: 0 L)(k: j j)(L: 0 (2j -3k))) not "natural" (see Section 2) infs j = infs k = infs L = o = sups j = sups k = sup k , INF(J,NIL) = INF(k,NIL) = INF(L,NIL) = O,s SUP(j,NIL) = SUP(L,NIL) = 0, SUP(k,NIL) =+ co .

(This is the naturalized form of 6.) SUP(k,NIL) = 0 . Other values of SUP and INF are 0 as in 6 .

1. S= ((k: 0 j}(j: 0 L}{L: 0 j-k+4}) . supS k = 4, SUP(k,NIL) = + ·' .

When S i s naturalized, SUP(k,NIL)=4.

1. S= ((J: 0 k+L}(k: 0 S)(L: 0 k)) . INF(j,NIL) = INF(k,NIL) = INF(L,NIL) = 0, SUP(j,NIL) = 10, SUP(k,NIL) = SUP(L,NIL) = 5. Acknowledgments. I am indebted to Mabry Tyson, Michael Ballantyne and Mark Moriconi for their help on this paper .

ALOORITHM SUP p 1 L)

ALGORITHM INF(J 1 L)

ALOORITll1 SUPP (x, y)

ALGORITHM INFF(x,y)

It is clear that the methods of integer programming [11) can be used to prove theorems of the type we consider here, and similarly our procedure can be thought of as another method for solving integer programming problems.