Formalization of continuous Functions in Topological Spaces using Isabelle/HOL
2011
This paper describes the formalization of continuous Functions in Topological Spaces using Isabelle, is an interactive theorem prover. Definitions and proofs of general topology are written in a computer language (Isabelle) so that they can be formally verified by machine. We formalize general topology in Isabelle/HOL to build formal mathematical libraries, which can improve the ability to automatically prove theorems.
Keywords:
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
9
References
0
Citations
NaN
KQI