关键词: 格蕴涵代数，格值命题逻辑系统LP(X)，自动推理，语义归结方法

Abstract: Resolution-based automated reasoning is one of most important research directions in AI, semantic method is one of the most important reform methods for resolution principle, in semantic resolution method, it utilizes the technology restraining the type of clauses and the order of literals participated in resolution procedure to reduce the redundant clauses,and can improve the efficiency of reasoning,a一resolution principle on lattice-valued logic based on lattice implicanon algebra provides a alternative tool to handle the automated reasoning problem with uncomparability and fuzziness inforr工ration. It can refutably prove the unsatisfiability of logical forr工mlae in lattico-valued logic syster工r. Firstly, this paper discussed the property of one class of generalized clause set on latticcvalucd propositional logic I_P(X)，this gcncr}r lined clause set can be divided into two non-empty sets, the semantic resolution method on it was investigated and sound theorem and weak complete theorem of this semantic resolution method were proved.

Key words: Latticc implication algcbra,I_atticcvalucd propositional logic I_P(X)，Automated reasoning, Semantic resolotion method