This library provides Roots, Powers and Generalized Logarithms. Hooks are provided so that the power function along with root and log can be shown to be continuous (over suitable domains), but no continuity libraries have been used to construct this library, meaning that it is built directly onto the standard SRI prelude. Features include:
- By importing
root, you can have statements like:root(8,3) = 2 - By importing
real_expt, you can have statements like:8^(1/3) = 2 - BY importing
log, you can have statements like:log(2)(8) = 3meaningln(8)/ln(2)
| Theorem | Location | PVS Name | Contributors |
|---|
- David Lester, Manchester University, UK
- César Muñoz, NASA, USA
- Sam Owre, SRI, USA
- Mariano Moscato, NIA & NASA, USA
- César Muñoz, NASA, USA
