Overview on Mechanized Theorem Proving

被引：0
作者：
Jiang N. [1 ]
Li Q.-A. [2 ]
Wang L.-M. [2 ]
Zhang X.-T. [2 ]
He Y.-X. [2 ]
机构：
[1] School of Computer Science, Hubei University of Technology, Wuhan
[2] School of Computer Science, Wuhan University, Wuhan
来源：
Ruan Jian Xue Bao/Journal of Software | 2020年 / 31卷 / 01期
基金：
中国国家自然科学基金;
关键词：
Logics of programming; Natural deduction; Proof assistant; Refinement; Resolution; Theorem proving; Typed; λ-calculus;
D O I：
10.13328/j.cnki.jos.005870
中图分类号：
学科分类号：
摘要：
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 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. © Copyright 2020, Institute of Software, the Chinese Academy of Sciences. All rights reserved.
引用
收藏
页码：82 / 112
页数：30
相关论文
共 184 条
[1]  
Paulson L.C., Computational logic: Its origins and applications, Proc. of the Royal Society A Mathematical Physical and Engineering Sciences, 474, 2210, (2018)
[2]  
Wu W.J., Mathematics Mechanization, (2003)
[3]  
Harrison J., Urban J., Wiedijk F., History of interactive theorem proving, Handbook of the History of Logic, 9, 2, pp. 135-214, (2014)
[4]  
Wang H., Toward mechanical mathematics, IBM Journal of Research and Development, 4, pp. 2-22, (1960)
[5]  
McCarthy J., Computer programs for checking mathematical proofs, Proc. of the 5th Symp. on Pure Mathematics of the American Mathematical Society, pp. 219-227, (1961)
[6]  
Wos L., Pereira F., Hong R., Boyer R.S., Moore J.S., Bledsoe W.W., Henschen L.J., Buchanan B.G., Wrightson G., Green C., An overview of automated reasoning and related fields, Journal of Automated Reasoning, 1, 1, pp. 5-48, (1985)
[7]  
Blazy S., Dargaye Z., Leroy X., Formal verification of a C compiler front-end, Proc. of the 14th Int'l Symp. on Formal Methods, pp. 460-475, (2006)
[8]  
Leroy X., A formally verified compiler back-end, Journal of Automated Reasoning, 43, 4, pp. 363-446, (2009)
[9]  
Demange B.D., Pichardie D., A formally verified SSA-based middle-end-Static single assignment meets CompCert, Proc. of the 21st European Conf. on Programming Languages and Systems, pp. 47-66, (2012)
[10]  
Klein G., Elphinstone K., Heiser G., Andronick J., Cock D., Derrin P., Elkaduwe D., Engelhardt K., Kolanski R., Norrish M., Sewell T., Tuch H., Winwood S., seL4: Formal verification of an OS kernel, Proc. of the 22nd Symp. on Operating Systems Principles, pp. 207-220, (2009)
12345678910