公开(公告)号：CN108875947A

公开(公告)日：2018-11-23

申请号：CN201710335858.7

申请日：2017-05-12

Applicant: 西南交通大学

Inventor： 徐扬 ,  何星星 ,  钟小梅 ,  陈树伟 ,  刘军

IPC: G06N5/04

Abstract: 本发明提出了一阶逻辑中基于标准延拓三角形的矛盾体分离多元动态自动演绎推理方法，该方法依次通过：构造基于标准延拓三角形矛盾体；形成矛盾体分离式；根据矛盾体分离式判断子句集属性，如果能够判断子句集不可满足或可满足，则停止；否则，将所得矛盾体分离式加入原子句集，形成新的子句集。接着构造并分离基于标准延拓三角形矛盾体，直至满足条件停止或得到子句集属性的判定结论。本发明提供了一阶逻辑中一种有效的基于矛盾体分离的动态自动演绎推理方法，实现将静态的、二元的归结演绎推理机制改进推广成为动态的、多元的基于矛盾体分离的演绎推理机制，是自动演绎推理领域一个本质性的突破。

公开(公告)号：CN108875946A

公开(公告)日：2018-11-23

申请号：CN201710335855.3

申请日：2017-05-12

Applicant: 西南交通大学

Inventor： 徐扬 ,  钟小梅 ,  刘军 ,  何星星 ,  陈树伟

IPC: G06N5/04

Abstract: 本发明公开了一阶逻辑中基于矛盾体分离的多元动态自动演绎推理方法，该方法通过在一阶逻辑中的子句集S中寻找标准矛盾体，然后在子句集S中剩余的子句中删除出现在标准矛盾体中的文字，并将全部剩余文字进行析取形成矛盾体分离式，最后根据矛盾体分离式判定初始的子句集S的属性，最终直到得出判定结果，则停止演绎推理。本发明可将静态的、二元的归结演绎推理机制改进推广成为动态的、多元的基于矛盾体分离的演绎推理机制，可应用于系统可信性自动验证、定理机器证明等领域，具有多元性、动态性、并行性、协调性、导向性、灵活性、方便性等特点。

公开(公告)号：CN108875945A

公开(公告)日：2018-11-23

申请号：CN201710335328.2

申请日：2017-05-12

Applicant: 西南交通大学

Inventor： 徐扬 ,  陈树伟 ,  刘军 ,  钟小梅 ,  何星星

IPC: G06N5/04

Abstract: 本发明公开了一阶逻辑中基于扩展三角形的矛盾体分离演绎推理方法，该方法依次通过：对于一阶逻辑中的子句集构造扩展三角形标准矛盾体，形成标准矛盾体分离式，根据标准矛盾体分离式判断子句集的不可满足性；如果能够判断子句集不可满足，则停止得到结论：被判定的子句集S不可满足；否则，将所得标准矛盾体分离式加入子句集S，形成新的子句集，然后重复构造扩展三角形标准矛盾体，并分离扩展三角形标准矛盾体，直至得到子句集S属性的判定结论或满足设定条件停止；本发明提供了一阶逻辑中一种有效的基于矛盾体分离的动态自动演绎推理方法，能有效刻画多个子句间的协同逻辑关系，并可应用于程序验证、定理机器证明等领域。