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
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
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
See also non-linear-arithmetic for a description of an extension to the linear-arithmetic procedure described here.