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

计算机工程与科学

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

曹锋1,3，徐扬2,3，吴贯锋1,3，钟建1,3

（1.西南交通大学信息科学与技术学院,四川成都 610031;2.西南交通大学数学学院,四川成都 610031;

3.系统可信性自动验证国家地方联合工程实验室,四川成都 610031）

收稿日期:2018-10-08 修回日期:2019-01-25 出版日期:2019-09-25 发布日期:2019-09-25
基金资助:
国家自然科学基金（61673320）;中央高校基本科研业务费专项资金（2682017ZT12,2682018CX59,2682018ZT25）

Application of multi-clause dynamic deduction in Prover9

CAO Feng1,3，XU Yang2,3，WU Guan-feng1,3，ZHONG Jian1,3

（1.School of Information Science and Technology,Southwest Jiaotong University,Chengdu 610031;

2.School of Mathematics,Southwest Jiaotong University,Chengdu 610031;

3.National-Local Joint Engineering Laboratory of System Credibility Automatic Verification,Chengdu 610031,China）

Received:2018-10-08 Revised:2019-01-25 Online:2019-09-25 Published:2019-09-25

摘要/Abstract

摘要：

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

关键词: 二元归结, 矛盾体分离, 多元动态演绎, 演绎权重

Abstract:

Prover9 only adopts the binary resolution method, which is a static and partial inference rule. Based on the contradiction separation rule, we propose a multi-clause dynamic deduction algorithm. This algorithm uses a holistic deduction framework, plans the deduction path according to clause deduction weight and literal deduction weight, and employs the backtracking mechanism to search for the optimal path. The Conference on Automated Deduction 2017 competition theorems (First-Order Form division) are used as the test object, and the theorems solved by the Prover9 with the multi-clause dynamic deduction algorithm is increased by 40.7%, and the average time used is reduced by 7.46 seconds. Experiments show that the proposed algorithm is an effective inference method, and can improve the ability of first-order logic automated theorem prover.

Key words: binary resolution, contradiction separation, multi-clause dynamic deduction, deduction weight

曹锋1,3，徐扬2,3，吴贯锋1,3，钟建1,3. 多元动态演绎在Prover9证明器中的应用[J]. 计算机工程与科学.

CAO Feng1,3，XU Yang2,3，WU Guan-feng1,3，ZHONG Jian1,3. Application of multi-clause dynamic deduction in Prover9[J]. Computer Engineering & Science.