The PVS development
`affine_arith`

formalizes the theory of affine arithmetic for expressions
involving constants, variables, addition, subtraction, multiplication,
and the power operation on variables. This development
includes the proof-producing strategy `aff-numerical`

for evaluating multivariate
polynomials with variables in interval domains.

- The Affine development is available as part of the NASA PVS Library.
- Examples.

- Mariano Moscato, César Muñoz, and Andrew Smith,
*Affine Arithmetic and Applications to Real-Number Proving*, Proceedings of the 6th International Conference on Interactive Theorem Proving (ITP 2015), Lecture Notes in Computer Science, Vol. 9236, pp. 294-309, 2015. BibTeX Reference.