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

• 作者: 关永 康漫 张杰 李晓娟
• 来源期刊: 计算机应用与软件
• 学科: 工学
• 关键词: 定理证明方法 形式化验证 定理证明器 证明方法 对策
• 年，卷（期）: 2017,（11）
• 所属期刊栏目: 软件技术与研究
• 页码范围: 6-12
• 页数: 7页
• 分类号: TP301.2
• 字数: 6995字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-386x.2017.11.002

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张杰	北京化工大学信息科学与技术学院	60	501	11.0	20.0
2	关永	首都师范大学信息工程学院	95	1336	17.0	33.0
3	李晓娟	首都师范大学信息工程学院	39	261	9.0	14.0
4	康漫	北京化工大学信息科学与技术学院	1	0	0.0	0.0