机械化定理证明研究综述

随着现代社会计算机化程度的提高，与计算机相关的各种系统故障足以造成巨大的经济损失.机械化定理证明能够建立更为严格的正确性，从而奠定系统的高可信性.针对机械化定理证明的逻辑基础和关键技术，详细剖析了一阶逻辑和基于消解的证明技术、自然演绎和类型化的λ演算、三种编程逻辑、基于高阶逻辑的硬件验证技术、程序构造和求精技术之间的联系和发展变迁，其中，三种编程逻辑包括一阶编程逻辑及变体、Floyd-Hoare逻辑和可计算函数逻辑.然后分析比较了各类主流证明助手的设计特点，阐述了几个具有代表性的证明助手的开发和实现.接下来对它们在数学、编译器验证、操作系统微内核验证、电路设计验证等领域的应用成果进行了仔细分析.最后，对机械化定理证明进行总结，并提出面临的挑战和未来研究方向.