[发明专利]命题逻辑中基于标准延拓三角形的矛盾体分离演绎推理

摘要

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

主权项

1.命题逻辑中基于标准延拓三角形的矛盾体分离演绎推理，其特征在于具体包括如下步骤：(一)对于命题逻辑中的子句集S＝{C1,C2,…,Cm}，综合考虑子句中文字数及互补文字所处的子句的指标，从子句集中选取k个子句，构造基于标准延拓三角形矛盾体；其中，C1,C2,…,Cm为命题逻辑中的子句；m是子句集S中子句的个数，k是选自子句集S用于构造矛盾体的子句个数；m≥2，k≥2；(二)将步骤(一)中所构造的基于标准延拓三角形矛盾体从参与构造的k个子句中删去，并将删去基于标准延拓三角形矛盾体后的k个子句中的剩余文字按析取关系组成新的子句，即矛盾体分离式；(三)利用步骤(二)中得到的矛盾体分离式，判定子句集的属性：如果能够判定子句集不可满足，则停止，得到结论：子句集S不可满足；如果能够判定子句集是可满足，则停止，得到结论：子句集S可满足，且能给出其可满足例；否则，将所得矛盾体分离式加入子句集S，形成新的子句集，然后重复步骤(一)，接着构造并分离基于标准延拓三角形矛盾体，直至得到子句集属性的判定结论。