| 机械化定理证明研究综述 |
| |
| 作者姓名： | 江南 李清安 汪吕蒙 张晓瞳 何炎祥 |
| |
| 作者单位： | 湖北工业大学计算机学院,湖北武汉430068;武汉大学计算机学院,湖北武汉430072 |
| |
| 基金项目： | 国家自然科学基金（90818018,91018009,61170022,91118003,61373039）;华为技术有限公司合作项目（YB2015090035）;湖北工业大学校博士科研启动基金（BSQD2017043）. |
| |
| 摘 要： | 随着现代社会计算机化程度的提高,与计算机相关的各种系统故障足以造成巨大的经济损失.机械化定理证明能够建立更为严格的正确性,从而奠定系统的高可信性.针对机械化定理证明的逻辑基础和关键技术,详细剖析了一阶逻辑和基于消解的证明技术、自然演绎和类型化的λ演算、3种编程逻辑、基于高阶逻辑的硬件验证技术、程序构造和求精技术之间的联系和发展变迁,其中,3种编程逻辑包括一阶编程逻辑及变体、Floyd-Hoare逻辑和可计算函数逻辑.然后分析、比较了各类主流证明助手的设计特点,阐述了几个具有代表性的证明助手的开发和实现.接下来对它们在数学、编译器验证、操作系统微内核验证、电路设计验证等领域的应用成果进行了细致的分析.最后,对机械化定理证明进行了总结,并提出面临的挑战和未来研究方向.
|
| 关 键 词： | 定理证明 证明助手 消解 自然演绎 类型化的λ演算 编程逻辑 求精 |
| 收稿时间： | 2018-07-20 |
| 修稿时间： | 2019-03-04 |
| 本文献已被 维普 万方数据 等数据库收录！ |
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
|
