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 and 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.
|68T15||Theorem proving (deduction, resolution, etc.)|
|03B35||Mechanical theorem proving; logical operations|
|26E35||Nonstandard real analysis|