Hi,
does anyone notice that, the 3 basic transcendental functions (sin, cos,
exp) in HOL4 are only correctly defined on positive inputs?
I say this because all these definitions are based on suminf which gives
desired results only for all positive summations:
[exp] Definition
⊢ ∀x.
Sorry... I'm wrong, these definitions are correct. I was confused by
the definition of "suminf" for reals with the one for extreals. The
one for reals is based on "sums" and "convergent", should be able to
handle negative values.
So, it should be possible to prove a full version of EXP_LE_X.
The Eleventh NASA Formal Methods Symposium
https://robonaut.jsc.nasa.gov/R2/pages/nfm2019.html
7 - 9 May 2019
Rice University, Houston, Texas, USA
*** Hotel
[ Apologize for Multiple Copies ]
***
DEADLINE EXTENDED
***
iFM 2019 - Call for Workshops and Tutorials
15th International Conference on
Formal Methods 2019 - Doctoral Symposium
Porto, Portugal, October 7th, 2019
http://formalmethods2019.inesctec.pt/?page_id=361
In conjunction with the
23rd International Symposium on Formal Methods and
3rd World Congress on Formal Methods
Porto, Portugal, October 7-11, 2019
The Eleventh NASA Formal Methods Symposium
https://robonaut.jsc.nasa.gov/R2/pages/nfm2019.html
7 - 9 May 2019
Rice University, Houston, Texas, USA
*** Hotel
==
Third and Final Call for Papers
FM 2019 - 23rd International Symposium on Formal Methods
- 3rd World Congress on Formal Methods
Porto, Portugal, October 7-11, 2019
http://formalmethods2019.inesctec.pt/
The 35th International Conference on Logic Programming (ICLP 2019)
Research Challenges in Logic Programming Track
September 21-25, 2019
Las Cruces, New Mexico (USA)
https://www.cs.nmsu.edu/ALP/iclp2019/
-
Objectives
Are you
