Linear arithmetic is the fragment of arithmetic built from equalities and inequalities between linear expressions , combined by logical operations and, in some versions, quantifiers. Coefficients are fixed numbers; multiplying two unknowns, as in , leaves this fragment. One must specify whether the unknowns range over the integers, rational numbers or real numbers.[ref]
For example, and are linear constraints. Substitution gives , hence . But has a real number solution and no integer solution, so a procedure for one number system cannot simply be reused for the other. This distinction makes linear arithmetic useful in automated reasoning about counts, schedules and bounds.
New to topics? Read the docs here!