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