机械化定理证明研究综述

• 作者: 何炎祥 张晓瞳 李清安 江南 汪吕蒙
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 定理证明 证明助手 消解 自然演绎 类型化的λ演算 编程逻辑 求精
• 年，卷（期）: 2020,（1）
• 所属期刊栏目: 模式识别与人工智能
• 页码范围: 82-112
• 页数: 31页
• 分类号: TP18
• 字数: 25924字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.005870

摘要

随着现代社会计算机化程度的提高,与计算机相关的各种系统故障足以造成巨大的经济损失.机械化定理证明能够建立更为严格的正确性,从而奠定系统的高可信性.针对机械化定理证明的逻辑基础和关键技术,详细剖析了一阶逻辑和基于消解的证明技术、自然演绎和类型化的λ演算、3种编程逻辑、基于高阶逻辑的硬件验证技术、程序构造和求精技术之间的联系和发展变迁,其中,3种编程逻辑包括一阶编程逻辑及变体、Floyd-Hoare逻辑和可计算函数逻辑.然后分析、比较了各类主流证明助手的设计特点,阐述了几个具有代表性的证明助手的开发和实现.接下来对它们在数学、编译器验证、操作系统微内核验证、电路设计验证等领域的应用成果进行了细致的分析.最后,对机械化定理证明进行了总结,并提出面临的挑战和未来研究方向.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	江南	湖北工业大学计算机学院	18	70	4.0	8.0
2	何炎祥	武汉大学计算机学院	179	1866	22.0	35.0
3	李清安	武汉大学计算机学院	18	35	5.0	5.0
4	张晓瞳	武汉大学计算机学院	4	6	2.0	2.0
5	汪吕蒙	武汉大学计算机学院	3	0	0.0	0.0