格值命题逻辑系统Ln×2P(X)中广义文字的α-归结性

α-Resolution Fields of Generalized Literals in Lattice-valued Propositional Logic L_(n×2)P(X)

归结自动推理是人工智能领域的一个重要研究方向.以格蕴涵代数为真值域的格值逻辑中的α-归结方法提供了一种处理带有模糊性和不可比较性信息的自动推理问题的工具,能对格值逻辑系统的α-不可满足子句集给出反驳证明,用α-归结原理证明格值逻辑中广义子句集的α-不可满足性,必须首先研究两个广义文字是否可以进行α-归结.研究了格值逻辑中一阶不可分极简式1-IESF和其他一些广义文字的α-归结性,得到了两个广义文字可进行α-归结的条件,以期能对基于格值逻辑的归结自动推理提供一些必要的理论支持.

Resolution based automatic reasoning is one of most important research directions in AI.α-resolution method on lattice-valued logic based on lattice implication algebra provides alternative tool to handle the automatic reasoning problem with incomparability and fuzziness of information.It can refutably prove the α-unsatisfiability of clause set in lattice-valued logic system.We need to judge whether or not two generalized literals can form α-resolution pairs when we use α-resolution principle to refutably prove the α-unsatisfiability of a clausal set in Ln×2P（X）.This paper discusses the resolvent of 1-IESF and other generalized literals and gets some determinations for α-resolution of two generalized literals.