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

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