A description of the linear arithmetic decision procedure

ACL2 incorporates a rational linear arithmetic decision procedure.
When the ACL2 prover attempts to simplify a goal, it first constructs a data
structure, called the ``linear pot list'' (see linear), that records
inequalities derived from the current goal, as an early step in the
simplification process. The linear pot list is constructed as follows: first,
it is seeded with equalities and inequalities about arithmetic terms occurring
in the goal to be proved; then, it is extended by instantiating `linear` lemmas about terms already in the pot list. The resulting pot list is
then supplied to the decision procedure when the rewriter is trying to
establish or refute an arithmetic equality or inequality. This happens, for
example, when an inequality occurs as a hypothesis of a rule being applied by
the rewriter. (For discussion of the rewriter in general, see introduction-to-rewrite-rules-part-1 and introduction-to-rewrite-rules-part-2.)

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 `<` or `<=`) relation between two linear
polynomials. Note that an equality may be considered as a pair of
inequalities; e.q.,

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*x

and we wish to prove that, given

p3: 0 <= a.

and looking for a contradiction.

Our first step will be to eliminate the variable

p4: 6*x + 14*a + 9 < 8 + 6*x

which, after cancellation, is:

p4: 14*a + 1 < 0.

If we then cross-multiply and add

p5: 1 <= 0,

a contradiction. Thus, we have proved that

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 canceled against
each other only when they have the same largest unknown. For instance, in the
above example we see that

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`
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.

- Linear-arithmetic-with-complex-coefficients
- Some books for reasoning about arithmetic expressions with complex coefficients