DocumentCode
2599376
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
Volume
2
fYear
2010
fDate
24-25 April 2010
Firstpage
458
Lastpage
461
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;
fLanguage
English
Publisher
ieee
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
Type
conf
DOI
10.1109/NSWCTC.2010.242
Filename
5480885
Link To Document