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

• 作者: 吴贯锋 常文静 徐扬 曹锋 陈树伟
• 来源期刊: 西南交通大学学报
• 学科: 工学
• 关键词: 数理逻辑 人工智能 定理证明 二元归结 矛盾体分离规则
• 年，卷（期）: 2020,（2）
• 页码范围: 401-408,427
• 页数: 9页
• 分类号: TP311.1
• 字数: 8098字
• 语种: 中文
• DOI: 10.3969/j.issn.0258-2724.20180800

摘要

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