Mathematical Theorem Machine Proving System Based on Coq -Machine Proving of the Factorization Theorem of Principal Ideal Domain

摘要：

　　The complete machine proving of the Factorization Theorem of Principal Ideal Domain in the abstract algebra is given by using the interactive theorem proving tool Coq.The proof process is done by using Coq,which fully embodies the Coq-based mathematics theorem machine proving system are readable,interactive and intelligent.The machine proving progress is rigorous and reliable.

关键词： Coq abstract algebra principal ideal domain unique factorization ring machine proving

作者: SHU Rundong YU Wensheng

作者单位: Beijing University of Posts and Telecommunications,Beijing 100876,China

会议类型: 国内会议

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

会议地点: 厦门

会议语种:英文

页码: 345-352

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