• DocumentCode
    2341811
  • 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
  • Volume
    2
  • fYear
    2011
  • fDate
    22-23 Oct. 2011
  • Firstpage
    20
  • Lastpage
    23
  • 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;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    System Science, Engineering Design and Manufacturing Informatization (ICSEM), 2011 International Conference on
  • Conference_Location
    Guiyang
  • Print_ISBN
    978-1-4577-0247-1
  • Type

    conf

  • DOI
    10.1109/ICSSEM.2011.6081277
  • Filename
    6081277
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=2341811