Title :
A Formal Proof of Pasting Lemma in Isabelle/HOL
Author :
Wang, Jianlin ; Chen, Liangyu ; Zeng, Zhenbing
Author_Institution :
Shanghai Key Lab. of Trustworthy Comput., East China Normal Univ., Shanghai, China
Abstract :
Pasting lemma is proved in Isabelle/HOL. General topology is formalized to express Pasting lemma. Topology definitions and proofs are written in a computer language so that they can be formally verified by machine. We formalize general topology in Isabelle/HOL to find out reasoning mechanisms in general topology. Our personal motivation to prove this lemma is to explore applications of different knowledge domains.
Keywords :
theorem proving; topology; Isabelle/HOL; formal proof; pasting lemma; Application software; Computer languages; Computer networks; Formal languages; Laboratories; Logic; Mathematics; Network topology; Software engineering; Wireless communication; Isabelle/HOL; component formal proof; general topology; pasting lemma;
Conference_Titel :
Networks Security Wireless Communications and Trusted Computing (NSWCTC), 2010 Second International Conference on
Conference_Location :
Wuhan, Hubei
Print_ISBN :
978-0-7695-4011-5
Electronic_ISBN :
978-1-4244-6598-9
DOI :
10.1109/NSWCTC.2010.242
