On the mechanization of real analysis in Isabelle/HOL. (English) Zbl 0974.68186
Aagaard, Mark (ed.) et al., Theorem proving in higher order logics. 13th international conference, TPHOLs 2000, Portland, OR, USA, August 14-18, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1869, 145-161 (2000).
Summary: Our recent, and still ongoing, development of real analysis in Isabelle/HOL is presented and compared, whenever instructive, to the one present in the theorem prover HOL. While most existing mechanizations of analysis only use the classical $\varepsilon$ and $\delta$ approach, ours uses notions from both nonstandard analysis and classical analysis. The overall result is an intuitive, yet rigorous, development of real analysis, and a relatively high degree of proof automation in many cases. For the entire collection see [Zbl 0944.00036
|68T15||Theorem proving (deduction, resolution, etc.)|
|03B35||Mechanical theorem proving; logical operations|
|26E35||Nonstandard real analysis|