Abstract
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 t and 5 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.
Cite
CITATION STYLE
Fleuriot, J. D. (2000). On the mechanization of real analysis in isabelle/hol. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1869, pp. 145–161). Springer Verlag. https://doi.org/10.1007/3-540-44659-1_10
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
