[发明专利]一阶逻辑中基于矛盾体分离的多元动态自动演绎推理方法

摘要

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

主权项

1.一阶逻辑中基于矛盾体分离的多元动态自动演绎推理方法，其特征在于包括如下步骤：对于一阶逻辑中的一个子句集S＝{C1，…，Ci，…，Cn}是，即S＝C1∧…∧Ci∧…∧Cn，所述Ci为子句，其中i＝1，2，…，n；第一步，在子句集S中选出k个子句Cj1，Cj2，…，Cjk，其中k≥2；当所述k个子句经过某个替换θ后，子句Cj1θ，Cj2θ，…，Cjkθ含有标准矛盾体，其中，替换的定义见书《基于归结方法的自动推理》第43页定义2.12；第二步，在子句Cj1θ，Cj2θ，…，Cjkθ中删除出现在标准矛盾体中的文字，并将全部剩余文字进行析取形成矛盾体分离式；第三步，判定初始的子句集S的属性：若得出判定结果，则停止；否则，将得到的矛盾体分离式并入子句集S中得到一个新子句集，并对所述新子句集继续进行第一步、第二步和第三步，直到得出判定结果。