-
公开(公告)号：CN108875949A
公开(公告)日：2018-11-23
申请号：CN201710335863.8
申请日：2017-05-12
Applicant: 西南交通大学
IPC: G06N5/04
Abstract: 本发明公开了一阶逻辑中基于矛盾体分离式的逆向并行演绎推理方法，该方法步骤为：对一阶逻辑中子句集S构造矛盾体并形成矛盾体分离式R，根据R判断演绎推理是否终止：如果判定S不可满足，则停止；否则，用R与S构造t个新子句集，然后对t个新子句集进行演绎推理得到结果Rj，如果Rj都是空子句，则S不可满足；否则，对不为空的Rj对应的新子句集循环前述步骤，直至得到S属性的判定结论或满足设定条件停止，从而实现演绎推理过程；本发明能动态分解矛盾体分离式，形成动态逆向演绎目标，实现对逻辑公式集属性判定的并行处理，有效指导演绎推理，提高基于矛盾体分离的动态自动演绎推理的效率；本发明可用于程序验证、定理机器证明等领域。
-
公开(公告)号：CN108875951A
公开(公告)日：2018-11-23
申请号：CN201710335867.6
申请日：2017-05-12
Applicant: 西南交通大学
IPC: G06N5/04
Abstract: 本发明公开了一阶逻辑中基于矛盾体内部子句的逆向并行演绎推理方法，该方法依次通过：对一阶逻辑中的子句集S构造矛盾体并形成矛盾体分离式，根据矛盾体分离式判断演绎推理是否终止：如果S不可满足，则停止；否则，抽取标准矛盾体内部子句以得到的t个子句为目标，分别对S进行演绎推理，如果能演绎出这t个子句，则停止演绎，得到结论：S不可满足；否则，循环如上过程，直至得到S属性的判定结论或满足设定条件停止；本发明能动态抽取标准矛盾体内部子句，形成动态逆向演绎目标，实现对逻辑公式集属性判定的并行处理，有效指导演绎推理，提高基于矛盾体分离的动态自动演绎推理系统的演绎效率；本发明可应用于程序验证、定理机器证明等领域。
-
公开(公告)号：CN108875943A
公开(公告)日：2018-11-23
申请号：CN201710335319.3
申请日：2017-05-12
Applicant: 西南交通大学
IPC: G06N5/04
Abstract: 本发明公开了命题逻辑中基于矛盾体分离的多元动态自动演绎推理方法，对于命题逻辑中子句集S，在S中选出k个子句Cj1，Cj2，…，Cjk，满足Cj1，Cj2，…，Cjk含有矛盾体；第二步，在子句Cj1，Cj2，…，Cjk中删除矛盾体中的文字，将全部剩余文字进行析取形成矛盾体分离式；最后，判定子句集S的属性：若得出判定结果，则停止，否则，将矛盾体分离式并入S中得到新子句集，并对新子句集执行前两步，直到得出结果。该方法可同时使用子句集中的多个甚至全部子句参与演绎，在更大程度上刻画了多子句之间的整体协同逻辑关系，是将静态的、二元的归结演绎推理机制改进推广成为动态的、多元的基于矛盾体分离的演绎推理机制。
-
公开(公告)号：CN108875941A
公开(公告)日：2018-11-23
申请号：CN201710334658.X
申请日：2017-05-12
Applicant: 西南交通大学
IPC: G06N5/04
Abstract: 本发明公开了命题逻辑中基于矛盾体分离式的逆向并行演绎推理方法，该方法步骤为：对命题逻辑中子句集S构造矛盾体并形成矛盾体分离式，根据矛盾体分离式判断S的不可满足性：如果判定S不可满足则停止，否则，基于矛盾体分离式构造逆向演绎子句集，得到t个新子句集并进行演绎推理，如果对t个新子句集的演绎结果都是空子句，则S不可满足，否则循环前述步骤，直至得到S属性的判定结论或满足设定条件停止；本发明能动态分解矛盾体分离式，形成动态逆向演绎目标，有效指导下一步演绎推理，并对分解后的逻辑公式集属性判定进行并行处理，有效提高基于矛盾体分离的动态自动演绎推理系统的演绎效率；本发明可用于程序验证、定理机器证明等领域。
-
公开(公告)号：CN108875940A
公开(公告)日：2018-11-23
申请号：CN201710334654.1
申请日：2017-05-12
Applicant: 西南交通大学
IPC: G06N5/04
Abstract: 本发明公开了命题逻辑中基于矛盾体内部子句的逆向并行演绎推理方法，该方法步骤为：对命题逻辑中子句集S构造矛盾体并形成矛盾体分离式，根据矛盾体分离式判断演绎推理是否终止：若矛盾体分离式为空则停止，得到结论：S不可满足；否则，抽取矛盾体内部子句并以所得t个子句为目标，分别对S进行演绎推理，若能演绎出这t个子句，则停止，得到结论：S不可满足；否则，循环如上过程，直至得到S属性的判定结论或满足设定条件停止；本发明能动态抽取矛盾体内部子句，形成动态逆向演绎目标，并对分解后的逻辑公式集属性判定进行并行处理，有效提高基于矛盾体分离的动态自动演绎推理系统的效率；本发明可应用于程序验证、定理机器证明等领域。
-
Patent Agency Ranking
公开(公告)号：CN108875944A
公开(公告)日：2018-11-23
申请号：CN201710335327.8
申请日：2017-05-12
Applicant: 西南交通大学
IPC: G06N5/04
Abstract: 本发明公开了命题逻辑中基于极大子句判定公式属性的方法，其步骤为：首先，根据子句集S中出现的所有命题变元集合V(S)，构造一个关于V(S)的极大子句D(k)，其次，在子句集S中将与子句～D(k)含有相同文字的子句删除，并将所得子句集记为S1，最后根据S1判定子句集S的属性；本发明给出了一种利用极大子句判定命题逻辑子句集属性的方法，且该方法在判定子句集为可满足的同时给出了一个满足该子句集的解释。
-
公开(公告)号：CN108875942A
公开(公告)日：2018-11-23
申请号：CN201710335313.6
申请日：2017-05-12
Applicant: 西南交通大学
IPC: G06N5/04
Abstract: 本发明提出了命题逻辑中基于标准延拓三角形的矛盾体分离演绎推理，该方法依次通过：构造基于标准延拓三角形矛盾体；形成矛盾体分离式；根据矛盾体分离式和子句的特点判定子句集属性，如果能够判断子句集不可满足或可满足，则停止；否则，将所得矛盾体分离式加入原子句集，形成新的子句集。接着构造并分离基于标准延拓三角形矛盾体，直至满足条件停止或得到子句集属性的判定结论。本发明可高效构造矛盾体，实现将静态的、二元的归结演绎推理机制改进推广成为动态的、多元的基于矛盾体分离的演绎推理机制，是自动演绎推理领域一个本质性的突破。
-
公开(公告)号：CN108875939A
公开(公告)日：2018-11-23
申请号：CN201710334627.4
申请日：2017-05-12
Applicant: 西南交通大学
IPC: G06N5/04
Abstract: 本发明公开了命题逻辑中基于最大矛盾体的自动推理方法，其步骤为：首先，利用子句集S中出现的k个变元生成最大矛盾体，然后利用最大矛盾体找出矛盾体，删除矛盾体中的文字后，将全部剩余文字析取形成矛盾体分离式，最后利用矛盾体分离式判定子句集S的属性，完成推理；本发明突破了传统的归结原理每次演绎“且只能有两个子句参与”的限制，将静态、二元、归结演绎发展为动态、多元、矛盾体分离演绎，该方法具有更强的针对性、更大的灵活性，判定逻辑公式属性的能力更强。
-
公开(公告)号：CN108875950A
公开(公告)日：2018-11-23
申请号：CN201710335866.1
申请日：2017-05-12
Applicant: 西南交通大学
IPC: G06N5/04
Abstract: 本发明公开了命题逻辑中基于扩展三角形的矛盾体分离演绎推理方法，该方法步骤为：对于命题逻辑中的子句集S构造扩展三角形矛盾体，形成矛盾体分离式，根据矛盾体分离式判断子句集属性；如果能判断子句集不可满足，则停止；否则，将所得矛盾体分离式加入原子句集，形成新的子句集，接着构造并分离扩展三角形矛盾体，直至得到子句集属性的判定结论或满足设定条件停止；本发明提供了命题逻辑中一种有效的基于矛盾体分离的动态自动演绎推理方法，能有效刻画多个子句间的协同逻辑关系，并可应用于程序验证、定理机器证明等领域。
-
公开(公告)号：CN108875948A
公开(公告)日：2018-11-23
申请号：CN201710335861.9
申请日：2017-05-12
Applicant: 西南交通大学
IPC: G06N5/04
Abstract: 本发明公开了命题逻辑中基于最大矛盾体判定公式属性的方法，其步骤为：首先，利用子句集S中出现的全部命题变元构造最大矛盾体，然后在最大矛盾体中寻找满足一定条件的子句D，最后根据子句D判定子句集S的属性；本发明在基于矛盾体分离的多元动态自动演绎推理理论基础上，给出了一种利用最大矛盾体判定命题逻辑子句集属性的方法，且该方法在判定子句集为可满足的同时给出了一个满足该子句集的解释。
-
-
-
-
-
-
-
-
-
Search Results
13
records
(took 0.052 seconds)
