多元协同演绎在一阶逻辑ATP中的应用

摘要：

一阶逻辑是数理逻辑中重要的分支,对其逻辑公式的自动推理是人工智能领域重要的研究热点之一.目前一阶逻辑自动定理证明大多采用二元归结方法,每次只有2个子句进行归结,只消去1组互补对,导致演绎归结式文字数较多,影响了演绎效率.为此,基于矛盾体分离规则提出了一种多元协同演绎算法,该算法每次允许多个子句进行协同演绎,消去多组互补对,从而演绎分离式文字数较少且可控,能有效提高推理能力;并且,该算法通过有效演绎权重和无效演绎权重调整子句演绎顺序,利用回溯机制搜索较优路径,有效规划演绎路径.将该算法应用于国际顶尖证明器Eprover 2.1,以CADE2017竞赛例(FOF组)为测试对象,对加入多元协同演绎算法的Eprover 2.1证明器进行试验.试验结果表明其能力超过了Eprover 2.1:多证明定理8个;能证明Eprover 2.1未证明定理31个,占未证明总数的28.2％.

关键词：数理逻辑、人工智能、定理证明、二元归结、矛盾体分离规则

所属期刊栏目：55

分类号：TP311.1(计算技术、计算机技术)

资助基金：国家自然科学基金;中央高校基本科研业务费专项资金

在线出版日期：2020-04-14（万方平台首次上网日期，不代表论文的发表时间）

页数：共9页

页码：401-408,427