Title :
Formalization of continuous Functions in Topological Spaces using Isabelle/HOL
Author :
Wang, Jianlin ; Chen, Liangyu ; Zeng, Zhenbing
Author_Institution :
Software Eng. Inst., East China Normal Univ., Shanghai, China
Abstract :
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 :
formal verification; theorem proving; Isabelle/HOL; computer language; continuous function; formal mathematical libraries; formal verification; formalization; interactive theorem prover; topological space; Software; HOL; Isabelle; continuous function; formalization; topology;
Conference_Titel :
System Science, Engineering Design and Manufacturing Informatization (ICSEM), 2011 International Conference on
Conference_Location :
Guiyang
Print_ISBN :
978-1-4577-0247-1
DOI :
10.1109/ICSSEM.2011.6081277
