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

摘要

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.%定理证明是形式化验证的主要方法之一,其中定理证明器的使用是难点.为了提高证明效率,论述HOL4系统中主要的三种证明方法:支持高级证明步骤.自动推理和化简器,为定理的证明提供了一个完整而通用的理论框架.详细说明了以上三种证明方法的相关对策的功能和应用环境,并为应用中可能出现的问题提出解决方案.给出的对策应用实例不仅体现了三种方法中相关对策的实用性,还进一步表明了提出解决方案的有效性.