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

摘要

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