江 南 , 李清安 , 汪吕蒙 , 张晓瞳 , 何炎祥

1(湖北工业大学 计算机学院,湖北 武汉 430068)

2(武汉大学 计算机学院,湖北 武汉 430072)

计算机已经渗透到社会生产和人类生活的方方面面,与计算机相关的各种故障足以造成巨大的经济损失.2017 年,全球爆发的勒索病毒(WannaCry)源于Windows 操作系统的漏洞(MS17-010);早在1994 年,奔腾处理器的浮点除运算错误使得英特尔公司不得不召回成百上千万芯片,损失约4.5 亿.更为严格的研发方法,能够避免许多这样的错误.在这些方法中,机械化定理证明是被学术界广泛认可的形式验证技术[1],并在工业界获得了越来越多的成功应用.

机械化定理证明是指使用计算机,以定理证明的方式对数学定理或计算机软、硬件系统进行形式验证,是人工智能(artificial intelligence,简称AI)的一种体现.Leibniz 早在17 世纪时就形成了由机器证明定理的思想,然而直到19 世纪末现代逻辑的创立和发展,以及20 世纪40 年代计算机的出现,才使得这一设想的实现具有了现实可能性[2].

始于20 世纪50 年代和60 年代,机械化定理证明围绕计算机如何高度自动化地完成证明而展开.受当时倡导的人工智能潜能的影响,自动定理证明(automated theorem proving,简称ATP)技术的研究经历了一段炽热的研发期,也取得了许多具有影响力的成果;但是随着新问题、新技术和新思想的到来,完全自动定理证明的研究渐入停滞期,对于大多数有意义的数学定理或计算机系统的正确性,交互式地进行证明可能是唯一可行的工作方式[3].

交互式定理……