Machine Proving System for Mathematical Theorems based on Coq-Machine Realization of the Axiomatic Set Theory
Using the interactive theorem proving tool Coq,we completed the construction of the machine proving system of the axiomatic set theory.The axiomatic set theory used in this paper refers to Kelley”s axiomatic set theory.Kelley”s axiomatic set theory is based on eight axioms and one axiom scheme,and it is free from the more obvious paradoxes.The system we developed has completed the proof of Kelley”s axiomatic set theory with Coq,including the description of eight axioms and one axiom schema and the description or proof of all 181 definitions or theorems with Coq.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 Kelly Formalization Mathematical Theorem Machine proving
Sun Tianyu
Beijing Key Laboratory of Work Safety Intelligent Monitoring,School of Electronic Engineering Beijing University of Posts and Telecommunications,Beijing 100876,China
国内会议
厦门
英文
315-325
2017-11-17（万方平台首次上网日期，不代表论文的发表时间）