Overview on Mechanized Theorem Proving
Author:
Affiliation:

Clc Number:

TP18

Fund Project:

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)

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    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.

    Reference
    Related
    Cited by
Get Citation

江南,李清安,汪吕蒙,张晓瞳,何炎祥.机械化定理证明研究综述.软件学报,2020,31(1):82-112

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:July 20,2018
  • Revised:March 04,2019
  • Adopted:
  • Online: August 12,2019
  • Published: January 06,2020
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063