Affine Arithmetic

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.

Downloads

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

Publications

• 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.

The tag identifies links that are outside the NASA domain