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

(α,β)-Generalized Lock Resolution of Intuitionistic Fuzzy Logic

作　　者：邹丽[1,2] 刘迪[1] 郑宏亮[1] 

机构地区：[1]辽宁师范大学计算机与信息技术学院,辽宁大连116081 [2]南京大学计算机软件新技术国家重点实验室,南京210023

出　　处：《计算机科学与探索》2015年第8期1004-1009,共6页Journal of Frontiers of Computer Science and Technology

基　　金：国家自然科学基金Nos.61105059;61175055;61173100~~

摘　　要：归结方法是定理自动证明的重要工具。为了简化直觉模糊命题逻辑的归结过程,基于直觉模糊命题逻辑归结原理的一般形式,提出了子句(α,β)-可满足和(α,β)-归结式的概念。研究了广义子句与其归结式的可满足性。在直觉模糊命题逻辑系统中给广义子句配锁,规定在做归结时各子句中被消去文字在该子句中的序号最小,由此建立了(α,β)-广义锁归结方法,并证明了该方法的可靠性和完备性。给出了直觉模糊逻辑的广义锁归结算法步骤,并通过实例说明了该方法的有效性。Resolution method is an important tool of theorem automated proving. To reduce the resolution process of intuitionistic fuzzy logic, this paper proposes the concepts of （α,β）-satisfiable and （α,β）-resolvent based on the general form of resolution principle of intuitionistic fuzzy logic. Firstly, this paper discusses the satisfiability problem of generalized clauses and resolvent. Then, this paper gives the indexes of generalized clauses in intuitionistic fuzzy logic system. Resolution is permitted only on the literals of the lowest index in each clause. Therefore, this paper introduces （α,β）-generalized lock resolution method in intuitionistic fuzzy logic system, and proves its soundness and completeness. Finally, this paper presents the step of resolution algorithm and illustrates the effectiveness of the proposed method by an example.

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

分 类 号：TP301[自动化与计算机技术—计算机系统结构]