基于高阶逻辑的定理证明方法及其对策的应用  

THEOREM PROVING METHOD BASED ON HIGHER ORDER LOGIC AND ITS APPLICATION

作　　者：康漫 张杰[1] 李晓娟[2] 关永[2] 

机构地区：[1]北京化工大学信息科学与技术学院,北京100029 [2]首都师范大学信息工程学院,北京100048

出　　处：《计算机应用与软件》2017年第11期6-12,共7页Computer Applications and Software

基　　金：国家自然科学基金项目(61572331;61373034)

摘　　要：定理证明是形式化验证的主要方法之一,其中定理证明器的使用是难点。为了提高证明效率,论述HOL4系统中主要的三种证明方法:支持高级证明步骤。自动推理和化简器,为定理的证明提供了一个完整而通用的理论框架。详细说明了以上三种证明方法的相关对策的功能和应用环境,并为应用中可能出现的问题提出解决方案。给出的对策应用实例不仅体现了三种方法中相关对策的实用性,还进一步表明了提出解决方案的有效性。The use of theorem proving system is always a difficult point in theorem proving method, and the theorem proving is one of the main methods of formal verification. In order to improve the efficiency of proof, three main methods of proof in HOL4 system are discussed： support for high-level proof steps, automated reasoning and simplification. This paper provided a complete and general theoretical framework for proving theorems. The function and application environment of the commonly used tactics in above methods were analyzed in detail. We proposed solutions to the problems in applications. The application of the proposed strategy not only reflects the practicability of the relative measures in the three methods, but also shows the effectiveness of the proposed solution.

关 键 词：定理证明方法 形式化验证 定理证明器 证明方法 对策 

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]