多元动态演绎在Prover9证明器中的应用

• 作者: 吴贯锋 徐扬 曹锋 钟建
• 来源期刊: 计算机工程与科学
• 学科: 工学
• 关键词: 二元归结 矛盾体分离 多元动态演绎 演绎权重
• 年，卷（期）: 2019,（9）
• 所属期刊栏目: 人工智能与数据挖掘
• 页码范围: 1686-1692
• 页数: 7页
• 分类号: TP311.1
• 字数: 8771字
• 语种: 中文
• DOI: 10.3969/j.issn.1007-130X.2019.09.022

摘要

Prover9证明器只采用二元归结方法,是一种静态的、局部的推理规则.基于矛盾体分离规则,提出了一种多元动态演绎算法,采用整体式演绎框架,通过子句演绎权重与文字演绎权重规划演绎路径,并带有回溯机制搜索较优路径.以CADE2017竞赛例(FOF组)进行测试,加入多元动态演绎算法的Prover9证明器证明定理总数提高了40.7％,且所用的平均时间降低了7.46 s.实验表明,提出的多元动态演绎算法是一种有效的推理方法,能有效提高一阶逻辑自动定理证明器的能力.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	徐扬	西南交通大学数学学院	186	1462	15.0	32.0
5	吴贯锋	西南交通大学信息科学与技术学院	4	4	1.0	2.0
9	曹锋	西南交通大学信息科学与技术学院	2	0	0.0	0.0