| 摘要: |
| 随着现代社会计算机化程度的提高，与计算机相关的各种系统故障足以造成巨大的经济损失.机械化定理证明能够建立更为严格的正确性，从而奠定系统的高可信性.针对机械化定理证明的逻辑基础和关键技术，详细剖析了一阶逻辑和基于消解的证明技术、自然演绎和类型化的λ演算、3种编程逻辑、基于高阶逻辑的硬件验证技术、程序构造和求精技术之间的联系和发展变迁，其中，3种编程逻辑包括一阶编程逻辑及变体、Floyd-Hoare逻辑和可计算函数逻辑.然后分析、比较了各类主流证明助手的设计特点，阐述了几个具有代表性的证明助手的开发和实现.接下来对它们在数学、编译器验证、操作系统微内核验证、电路设计验证等领域的应用成果进行了细致的分析.最后，对机械化定理证明进行了总结，并提出面临的挑战和未来研究方向. |
| 关键词: 定理证明 证明助手 消解 自然演绎 类型化的λ演算 编程逻辑 求精 |
| DOI：10.13328/j.cnki.jos.005870 |
| 分类号:TP18 |
| 基金项目:国家自然科学基金（90818018，91018009，61170022，91118003，61373039）；华为技术有限公司合作项目（YB2015090035）；湖北工业大学校博士科研启动基金（BSQD2017043） |
|
| Overview on Mechanized Theorem Proving |
|
JIANG Nan1, LI Qing-An2, WANG Lü-Meng2, ZHANG Xiao-Tong2, HE Yan-Xiang2
|
|
1.School of Computer Science, Hubei University of Technology, Wuhan 430068, China;2.School of Computer Science, Wuhan University, Wuhan 430072, China
|
| 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. |
| Key words: theorem proving proof assistant resolution natural deduction typed λ-calculus logics of programming refinement |
