Major Section: RULE-CLASSES

See rule-classes for a general discussion of rule classes and
how they are used to build rules from formulas. An example
`:`

`corollary`

formula from which a `:linear`

rule might be built is:

Example: (implies (and (eqlablep e) if inequality reasoning begins to (true-listp x)) consider how (length (member a b)) (>= (length x) compares to any other term, add to (length (member e x)))) set of known inequalities the fact that it is no larger than (length b), provided (eqlablep a) and (true-listp b) rewrite to tNote: OneGeneral Form: (and ... (implies (and ...hi...) (implies (and ...hk...) (and ... (rel lhs rhs) ...))) ...)

`:linear`

rule class object might create many linear
arithmetic rules from the `:`

`corollary`

formula. To create the rules,
we first flatten the `and`

and `implies`

structure of the formula,
transforming it into a conjunction of formulas, each of the form
(implies (and h1 ... hn) (rel lhs rhs))where no hypothesis is a conjunction and

`rel`

is one of the
inequality relations `<`

, `<=`

, `=`

, `>`

, or `>=`

. If necessary, the
hypothesis of such a conjunct may be vacuous.
We create a `:linear`

rule for each such conjunct, if possible, and
otherwise cause an error. Each rule has one or more ``trigger
terms'' which may be specified by the user using the `:trigger-terms`

field of the rule class or which may be defaulted to values chosen
by the system. We discuss the determination of trigger terms after
discussing how linear rules are used.

`:linear`

rules are used by a linear arithmetic decision procedure
during rewriting. 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.
In our case, 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. Certain linear polynomial
inequalities can be combined by cross-multiplication and addition to
permit the deduction of a third linear inequality polynomial with
fewer unknowns. If this deduced inequality is manifestly false, a
contradiction has been deduced from the assumed inequalities.

For example, suppose we have three assumptions:

p1: 3*x + 7*a < 4 p2: 3 < 2*x p3: 0 <= a.By cross-multiplying and adding the first two (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 a polynomial must be eliminated by
cancellation in order to produce a constant inequality. We can
choose to eliminate the unknowns in any order. We eliminate them in
term-order, largest unknowns first. (See term-order.) 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 additional cancellation. 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 data base of `:linear`

rules for rules about
the unknowns that are candidates for cancellation (i.e., are the
largest unknowns in their respective inequalities).

If the trigger term of some `:linear`

rule can be instantiated to
yield a candidate for cancellation, we so instantiate that rule,
attempt to relieve the hypotheses with general-purpose rewriting,
and, if successful, convert the concluding inequality into a
polynomial inequality and add it to the set. This may let
cancellation continue. See the discussion of ``Linear Arithmetic
Rules'' pp 242 of A Computational Logic Handbook for more details.

We now describe how the trigger terms are determined. Most of the
time, the trigger terms are not specified by the user and are
instead selected by the system. However, the user may specify the
terms by including an explicit `:trigger-terms`

field in the rule
class, e.g.,

General Form of a Linear Rule Class: (:LINEAR :COROLLARY formula :TRIGGER-TERMS (term1 ... termk))Each

`termi`

must be a term and must not be a variable, quoted
constant, lambda application, `let-expression`

or `if-expression`

. In
addition, each `termi`

must be such that if all the variables in the
term are instantiated and then the hypotheses of the corollary
formula are relieved (possibly instantiating additional free
variables), then all the variables in the concluding inequality are
instantiated. We generate a linear rule for each conjuctive branch
through the corollary and store each rule under each of the
specified triggers. Thus, if the corollary formula contains several
conjuncts, the variable restrictions on the `termi`

must hold for each
conjunct.
Note: Problems may arise if you explicitly store a linear lemma
under a trigger term that, when instantiated, is not the largest
unknown in the instantiated concluding inequality. Suppose for
example you store the linear rule `(<= (fn i j) (/ i (* j j)))`

under
the trigger term `(fn i j)`

. Then when the system ``needs'' an
inequality about `(fn a b)`

, i.e., because `(fn a b)`

is the largest
unknown in some inequality in the set of assumed inequalities, it
will appeal to the rule and deduce `(<= (fn a b) (/ a (* b b)))`

.
However, the largest unknown in this inequality is `(/ a (* b b))`

and
hence this inequality will not be used until that term is eliminated
by cancellation with some other inequality. It is generally best to
specify as a trigger term one of the ``maximal'' terms of the
polynomial, as described below.

If `:trigger-terms`

is omitted the system computes a set of trigger
terms. Each conjunct of the corollary formula may be given a unique
set of triggers depending on the variables that occur in the
conjunct and the addends that occur in the concluding inequality.
In particular, the trigger terms for a conjunct is the list of all
``maximal addends'' in the concluding inequality.

The ``addends'' of `(+ x y)`

and `(- x y)`

are the union of the
addends of `x`

and `y`

. The addends of `(- x)`

and `(* n x)`

,
where `n`

is a numeric constant, is in all cases just `{x}`

. The
addends of an inequality are the union of the addends of the left-
and right-hand sides. The addends of any other term, `x`

, is
`{x}`

.

A term is maximal for a conjunct `(implies hyps concl)`

of the
corollary if (a) the term is a non-variable, non-quote, non-lambda
application, non-`let`

and non-`if`

expression, (b) the term contains
enough variables so that when they are instantiated and the
hypotheses are relieved then all the variables in `concl`

are
instantiated, and (c) any instantiation of the term is always at
least as ``large'' (see term-order for a description of the
order used) as the corresponding instantiations of any other addend
in `concl`

.