Abstract: Because of the complexity of generalized literals structure in lattice-valued logic, it leads to difficult to judge two generalized literals whether form resolution pair or not. According to particular structure of truth valued range[ Ln×L2] and the characteristic of resolution level α, the resolvability of between 0-IESF and other generalized literals in lattice-valued propositional logic system[ (Ln×L2)P(X) ]based on one class of lattice implication algebras[ Ln×L2], and the determination conditions on that two generalized literals can form resolution pair.

Key words: automated reasoning, resolution fields, lattice-valued logic, lattice implication algebras

摘要： 由于格值逻辑中广义文字结构的复杂性，这必然增加判断两个广义文字是否为α-归结对的难度。根据真值域[Ln×L2]的结构特性和归结水平[α]的特点，研究了真值域为一类格蕴涵代数[Ln×L2]的格值命题逻辑系统[(Ln×L2)P(X)]中0-IESF与其他广义文字之间的α-归结性，得到了两个广义文字可进行α-归结的条件。

关键词: 自动推理, 归结域, 格值逻辑, 格蕴涵代数