Abstract
We give a formalization of affine forms as abstract representations of zonotopes.
We provide affine operations as well as overapproximations of some non-affine operations like multiplication and division.
Expressions involving those operations can automatically be turned into (executable) functions approximating the original
expression in affine arithmetic.
License
History
- September 20, 2017
- linear approximations for all symbols from the floatarith data type
- January 31, 2015
- added algorithm for zonotope/hyperplane intersection
Topics
Session Affine_Arithmetic
- Affine_Arithmetic_Auxiliarities
- Executable_Euclidean_Space
- Affine_Form
- Floatarith_Expression
- Straight_Line_Program
- Affine_Approximation
- Counterclockwise
- Counterclockwise_Vector
- Counterclockwise_2D_Strict
- Polygon
- Counterclockwise_2D_Arbitrary
- Intersection
- Affine_Code
- Optimize_Integer
- Optimize_Float
- Float_Real
- Ex_Affine_Approximation
- Ex_Ineqs
- Ex_Inter
- Affine_Arithmetic