[发明专利]一阶逻辑中基于矛盾体分离式的逆向并行演绎推理方法

摘要

本发明公开了一阶逻辑中基于矛盾体分离式的逆向并行演绎推理方法，该方法步骤为：对一阶逻辑中子句集S构造矛盾体并形成矛盾体分离式R，根据R判断演绎推理是否终止：如果判定S不可满足，则停止；否则，用R与S构造t个新子句集，然后对t个新子句集进行演绎推理得到结果R_j，如果R_j都是空子句，则S不可满足；否则，对不为空的R_j对应的新子句集循环前述步骤，直至得到S属性的判定结论或满足设定条件停止，从而实现演绎推理过程；本发明能动态分解矛盾体分离式，形成动态逆向演绎目标，实现对逻辑公式集属性判定的并行处理，有效指导演绎推理，提高基于矛盾体分离的动态自动演绎推理的效率；本发明可用于程序验证、定理机器证明等领域。

主权项

1.一阶逻辑中基于矛盾体分离式的逆向并行演绎推理方法，其特征在于包括如下步骤：(一)构造标准矛盾体并形成矛盾体分离式：对于一阶逻辑中的子句集S＝{C₁,C₂,…,C_m}，其中C₁,C₂,…,C_m为一阶逻辑中的子句；从子句集S中选取k个子句D₁,…,D_i,…,D_k，对子句D_i依次做替换σ_i，D_i做替换后分成两个部分子句和构造标准矛盾体并形成矛盾体分离式其中，m是子句集S中子句的个数，k是选自子句集S用于构造标准矛盾体的子句个数；m≥2，k≥2；：i＝1，2，…，k；(二)根据矛盾体分离式判断演绎推理是否终止：如果步骤(一)所得的矛盾体分离式不是基子句，则返回步骤(一)，否则，如果所得矛盾体分离式为基子句，则判断子句集的不可满足性：如果矛盾体分离式为空，则停止，得到结论：子句集S不可满足；否则，转到步骤(三)；(三)基于矛盾体分离式构造逆向演绎子句集：根据步骤(一)选择矛盾体分离式R，记其中，y_j是一阶逻辑中的文字，t是矛盾体分离式中文字的个数，t≥1，j＝1，…，t；用矛盾体分离式R与子句集S协同构造t个新子句集S'，S'＝S∪{y_j}，然后转到步骤(四)；(四)并行演绎推理：对步骤(三)中得到的t个新子句集S'进行并行演绎推理或者逐个进行演绎推理，分别得到相应的演绎推理结果Rj；如果得到的Rj都是空子句，则得到结论：子句集S不可满足；否则，对子句集S或不是空子句的所有Rj对应的新子句集S'再次进行步骤(一)～(四)的演绎推理，直至得到子句集S不可满足性的判定结论，或达到设定的条件，则停止演绎推理，给出结论：子句集S属性无法判定。