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

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

Application of multi-clause dynamic deduction in Prover9

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.