Journal of Software:2020.31(1):82-112

(湖北工业大学 计算机学院, 湖北 武汉 430068;武汉大学 计算机学院, 湖北 武汉 430072)
Overview on Mechanized Theorem Proving
JIANG Nan,LI Qing-An,WANG Lü-Meng,ZHANG Xiao-Tong,HE Yan-Xiang
(School of Computer Science, Hubei University of Technology, Wuhan 430068, China;School of Computer Science, Wuhan University, Wuhan 430072, China)
Chart / table
Similar Articles
Article :Browse 2830   Download 2902
Received:July 20, 2018    Revised:March 04, 2019
> 中文摘要: 随着现代社会计算机化程度的提高,与计算机相关的各种系统故障足以造成巨大的经济损失.机械化定理证明能够建立更为严格的正确性,从而奠定系统的高可信性.针对机械化定理证明的逻辑基础和关键技术,详细剖析了一阶逻辑和基于消解的证明技术、自然演绎和类型化的λ演算、3种编程逻辑、基于高阶逻辑的硬件验证技术、程序构造和求精技术之间的联系和发展变迁,其中,3种编程逻辑包括一阶编程逻辑及变体、Floyd-Hoare逻辑和可计算函数逻辑.然后分析、比较了各类主流证明助手的设计特点,阐述了几个具有代表性的证明助手的开发和实现.接下来对它们在数学、编译器验证、操作系统微内核验证、电路设计验证等领域的应用成果进行了细致的分析.最后,对机械化定理证明进行了总结,并提出面临的挑战和未来研究方向.
Abstract:Modern society is now being increasingly computerized. Computer-related failures could result in severe economic loss. Mechanized theorem proving is an approach to ensuring stricter correctness, and hence high trustworthiness. First, the logical foundations and key technologies of mechanized theorem proving are discussed. Specifically, first-order logic and resolution-based technology, natural deduction and Curry-Howard correspondence, three logics of programming including first-order programming logic and its variant, FloydHoare logic, and logic for computable functions, hardware verification technology based on higher-order logic, and program constructions and refinement are analyzed, as well as the relationship and evolvement between them. Then key design features of the mainstream proof assistants are compared, and the development and implementation of several representative provers are discussed. Next their applications in the fields of mathematics, compiler verification, operating-system microkernel verification, and circuit design verification are analyzed. Finally, mechanized theorem proving is summarized and challenges and future research directions are put forward.
文章编号:     中图分类号:TP18    文献标志码:
基金项目:国家自然科学基金(90818018,91018009,61170022,91118003,61373039);华为技术有限公司合作项目(YB2015090035);湖北工业大学校博士科研启动基金(BSQD2017043) 国家自然科学基金(90818018,91018009,61170022,91118003,61373039);华为技术有限公司合作项目(YB2015090035);湖北工业大学校博士科研启动基金(BSQD2017043)
Foundation items:National Natural Science Foundation of China (90818018, 91018009, 61170022, 91118003, 61373039); HuaweiTechnologies Co. Ltd Project (YB2015090035); Doctoral Research Startup Foundation of Hubei University of Technology (BSQD2017043)
Reference text:


JIANG Nan,LI Qing-An,WANG Lü-Meng,ZHANG Xiao-Tong,HE Yan-Xiang.Overview on Mechanized Theorem Proving.Journal of Software,2020,31(1):82-112