Abstract: 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.

Key words: automated reasoning, intuitionistic fuzzy logic, (α,β)-generalized lock resolution, completeness theorem

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

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