Machine Proving System for Mathematical Theorems in Coq-Machine Proving of Tukey Lemma

摘要：

　　Under the axiomatic set theory frame,this paper implements the machine proving of the equivalence between the Axiom of Choice and Tukey lemma using Coq as an interactive theorem proving tool.The proving process demonstrates that the Coq-based machine proving of mathematics theorem is highly readable,interactive,rigorous and reliable.

关键词： Coq The axiomatic set theory Axiom of Choice Tukey lemma Equivalence Machine proving

作者: Sun Tianyu Yu Wensheng

作者单位: Beijing Key Laboratory of Work Safety Intelligent Monitoring,School of Electronic Engineering Beijing University of Posts and Telecommunications,Beijing 100876,China

会议类型: 国内会议

会议名称: 2017中国智能物联系统会议

会议地点: 厦门

会议语种:英文

页码: 372-378

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