Formalization of Kuratowski Closure Operation in Isabelle HOL

摘要：

This paper describes the formalization of Kuratowski closure operation in the higher order logic of Isabeile, is an interactive theorem prover. The formalization of Kuratowski closure operation is a part of the formalization of general topology, which definitions and proofs in general topology 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, which many mechanized proofs and formalization issues are discussed.

关键词： component Isabelle HOL topology formalization kuratowski closure operation

作者: Jianlin Wang Liangyu Chen Zhenbing Zeng

作者单位: Software Engineering Institute East China Normal University Shanghai, China

会议类型: 国际会议

会议名称: 2010 International Conference on Future Information Technology(2010年未来信息技术国际会议 ICFIT 2010)

会议地点: 长沙

会议语种:英文

页码: 263-266

在线出版日期: 2010-12-14（万方平台首次上网日期，不代表论文的发表时间）