Major Section: MISCELLANEOUS
We describe the procedure very roughly here.
Fundamental to the procedure is the notion of a linear polynomial
inequality. A ``linear polynomial'' is a sum of terms, each of
which is the product of a rational constant and an ``unknown.'' The
``unknown'' is permitted to be 1 simply to allow a term in the sum
to be constant. Thus, an example linear polynomial is
3*x + 7*a + 2; here x and a are the (interesting) unknowns.
However, the unknowns need not be variable symbols. For
example, (length x) might be used as an unknown in a linear
polynomial. Thus, another linear polynomial is 3*(length x) + 7*a.
A ``linear polynomial inequality'' is an inequality
(either < or <=)
relation between two linear polynomials. Note that an equality may
be considered as a pair of inequalities; e.q., 3*x + 7*a + 2 = 0
is the same as the conjunction of 3*x + 7*a + 2 <= 0 and
0 <= 3*x + 7*a + 2.
Certain linear polynomial inequalities can be combined by cross-multiplication and addition to permit the deduction of a third inequality with fewer unknowns. If this deduced inequality is manifestly false, a contradiction has been deduced from the assumed inequalities.
For example, suppose we have two assumptions
p1: 3*x + 7*a < 4 p2: 3 < 2*xand we wish to prove that, given
p1 and p2, a < 0. As
suggested above, we proceed by assuming the negation of our goal
p3: 0 <= a.and looking for a contradiction.
By cross-multiplying and adding the first two inequalities, (that is,
multiplying p1 by 2, p2 by 3 and adding the respective
sides), we deduce the intermediate result
p4: 6*x + 14*a + 9 < 8 + 6*xwhich, after cancellation, is:
p4: 14*a + 1 < 0.If we then cross-multiply and add
p3 to p4, we get
p5: 1 <= 0,a contradiction. Thus, we have proved that
p1 and p2 imply the
negation of p3.All of the unknowns of an inequality must be eliminated by
cancellation in order to produce a constant inequality. We can
choose to eliminate the unknowns in any order, but we eliminate them in
term-order, largest unknowns first. (See term-order.) That is, two
polys are cancelled against each other only when they have the same
largest unknown. For instance, in the above example we see that x
is the largest unknown in each of p1 and p2, and a in
p3 and p4.
Now suppose that this procedure does not produce a contradiction but
instead yields a set of nontrivial inequalities. A contradiction
might still be deduced if we could add to the set some additional
inequalities allowing further cancellations. That is where
:linear lemmas come in. When the set of inequalities has stabilized
under cross-multiplication and addition and no contradiction is
produced, we search the database of :linear rules for rules about
the unknowns that are candidates for cancellation (i.e., are the
largest unknowns in their respective inequalities). See linear
for a description of how :linear rules are used.
See also non-linear-arithmetic for a description of an extension
to the linear-arithmetic procedure described here.
