主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2019年第11期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
江南,李清安,汪吕蒙,张晓瞳,何炎祥.机械化定理证明研究综述.软件学报,2020,31(1):0
机械化定理证明研究综述
Mechanized theorem proving: A Survey
投稿时间:2018-07-20  修订日期:2019-03-04
DOI:10.13328/j.cnki.jos.005870
中文关键词:  定理证明  证明助手  消解  自然演绎  类型化的λ演算  编程逻辑  求精
英文关键词:theorem proving  proof assistant  resolution  natural deduction  typed λ-calculus  logics of programming  refinement
基金项目:国家自然科学基金(90818018,91018009,61170022,91118003,61373039);华为技术有限公司合作项目(YB2015090035);湖北工业大学校博士科研启动基金(BSQD2017043).
作者单位E-mail
江南 湖北工业大学 计算机学院, 湖北 武汉 430068  
李清安 武汉大学 计算机学院, 湖北 武汉 430070  
汪吕蒙 武汉大学 计算机学院, 湖北 武汉 430070  
张晓瞳 武汉大学 计算机学院, 湖北 武汉 430070  
何炎祥 武汉大学 计算机学院, 湖北 武汉 430070 yxhe@whu.edu.cn 
摘要点击次数: 957
全文下载次数: 511
中文摘要:
      随着现代社会计算机化程度的提高,与计算机相关的各种系统故障足以造成巨大的经济损失.机械化定理证明能够建立更为严格的正确性,从而奠定系统的高可信性.针对机械化定理证明的逻辑基础和关键技术,详细剖析了一阶逻辑和基于消解的证明技术、自然演绎和类型化的λ演算、三种编程逻辑、基于高阶逻辑的硬件验证技术、程序构造和求精技术之间的联系和发展变迁,其中,三种编程逻辑包括一阶编程逻辑及变体、Floyd-Hoare逻辑和可计算函数逻辑.然后分析比较了各类主流证明助手的设计特点,阐述了几个具有代表性的证明助手的开发和实现.接下来对它们在数学、编译器验证、操作系统微内核验证、电路设计验证等领域的应用成果进行了仔细分析.最后,对机械化定理证明进行总结,并提出面临的挑战和未来研究方向.
英文摘要:
      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, Floyd-Hoare 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 application in the field 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.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会 京ICP备05046678号-4
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利