This library provides a formalization of the Riemann definition of the integral of a function on an given interval.
| Theorem | Location | PVS Name | Contributors |
|---|
(riemann-numerical (&optional (breaks 12) (precision 2))
If the sequent contains un expression of form integral(A, B, EXPR), the strategy computes an interval containing the value of the integral of EXPR over the interval [A,B].
The parameter precision is used to determine the size of the output interval and breaks indicates the number of regions to use in the Riemann sum.
In particular, the sum will use 2^breaks regions.
- César Muñoz, NASA, USA
- Amer Tahat, Michigan Technological University, USA
- Gregory Anderson, University of Texas at Austin, USA
- Mariano Moscato, NIA & NASA, USA
- Sam Owre, SRI, USA
- César Muñoz, NASA, USA
