命题逻辑中基于扩展三角形的矛盾体分离演绎推理方法

摘要

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