计算机应用与软件2017，Vol.34Issue(11)：6-12,7.DOI:10.3969/j.issn.1000-386x.2017.11.002
基于高阶逻辑的定理证明方法及其对策的应用
THEOREM PROVING METHOD BASED ON HIGHER ORDER LOGIC AND ITS APPLICATION
摘要
Abstract
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.关键词
定理证明方法/形式化验证/定理证明器/证明方法/对策Key words
Theorem proving method/Formal verification/Theorem proving system/Proof method/Strategy分类
信息技术与安全科学引用本文复制引用
康漫,张杰,李晓娟,关永..基于高阶逻辑的定理证明方法及其对策的应用[J].计算机应用与软件,2017,34(11):6-12,7.基金项目
国家自然科学基金项目(61572331,61373034). （61572331,61373034）
