|
|||||
|
|
| 多元协同演绎在一阶逻辑ATP中的应用 | |
| 作者姓名： | 曹锋 徐扬 陈树伟 吴贯锋 常文静 |
| 基金项目： | 国家自然科学基金（61673320）;中央高校基本科研业务费专项资金（2682017ZT12,2682018CX59,2682018ZT25） |
| 摘 要： | 一阶逻辑是数理逻辑中重要的分支,对其逻辑公式的自动推理是人工智能领域重要的研究热点之一. 目前一阶逻辑自动定理证明大多采用二元归结方法,每次只有2个子句进行归结,只消去1组互补对,导致演绎归结式文字数较多,影响了演绎效率. 为此,基于矛盾体分离规则提出了一种多元协同演绎算法,该算法每次允许多个子句进行协同演绎,消去多组互补对,从而演绎分离式文字数较少且可控,能有效提高推理能力;并且,该算法通过有效演绎权重和无效演绎权重调整子句演绎顺序,利用回溯机制搜索较优路径,有效规划演绎路径. 将该算法应用于国际顶尖证明器Eprover 2.1,以CADE2017竞赛例（FOF组）为测试对象,对加入多元协同演绎算法的Eprover 2.1证明器进行试验. 试验结果表明其能力超过了Eprover 2.1:多证明定理8个;能证明Eprover 2.1未证明定理31个,占未证明总数的28.2%. |
| 关 键 词： | 数理逻辑 人工智能 定理证明 二元归结 矛盾体分离规则 |
| 收稿时间： | 2018-09-11 |
| 本文献已被 CNKI 等数据库收录！ | |
| 点击此处可从《西南交通大学学报》浏览原始摘要信息 | |
| 点击此处可从《西南交通大学学报》下载全文 | |