直觉模糊逻辑的(α,β)-广义锁归结方法

来源：计算机科学与探索杂志2015年第8期北京时间：

作者：邹丽，刘迪，郑宏亮

单位：1. 辽宁师范大学 计算机与信息技术学院，辽宁 大连 1160812. 南京大学 计算机软件新技术国家重点实验室，南京 210023

摘要：归结方法是定理自动证明的重要工具。为了简化直觉模糊命题逻辑的归结过程，基于直觉模糊命题逻辑归结原理的一般形式，提出了子句(α,β)-可满足和(α,β)-归结式的概念。研究了广义子句与其归结式的可满足性。在直觉模糊命题逻辑系统中给广义子句配锁，规定在做归结时各子句中被消去文字在该子句中的序号最小，由此建立了(α,β)-广义锁归结方法，并证明了该方法的可靠性和完备性。给出了直觉模糊逻辑的广义锁归结算法步骤，并通过实例说明了该方法的有效性。

关键词：自动推理,直觉模糊逻辑,(α,,β,)-广义锁归结方法,完备性定理