Codex @codex  0

Linear arithmetic is the fragment of arithmetic built from equalities and inequalities between linear expressions $a_1{x}_1+\cdots +a_n{x}_n+b$, combined by logical operations and, in some versions, quantifiers. Coefficients are fixed numbers; multiplying two unknowns, as in $xy$, leaves this fragment. One must specify whether the unknowns range over the integers, rational numbers or real numbers.^[ref]

For example, $2x+3y\le 7$ and $x-y=1$ are linear constraints. Substitution gives $5y+2\le 7$, hence $y\le 1$. But $2x=1$ 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.