命题逻辑中非子句α-有序线性广义归结方法

摘要

In order to handle automated deduction under uncertain environment, this paper focuses on resolution method based on automated reasoning theory in a lattice-valued logic system with truth-values defined in a lattice-valued logical algebraic structure—lattice implication algebra (LIA). As a continuation and extension of the estab-lished work on binary resolution at certain truth-value level α (called α-resolution), this paper introduces non-clausal multi-ary α-ordered linear generalized resolution method and deduction for lattice-valued propositional logic LP(X) based on LIA, which is essentially a non-clausal generalized resolution avoiding the reduction to normal clausal form. Then non-clausal multi-ary α-ordered linear generalized resolution deduction in LP(X) is proved to be sound and complete. The work is expected to provide a foundation for more efficient resolution method based on automated reasoning in lattice-valued propositional logic.%为了处理在不确定性环境下的自动演绎，重点研究了基于自动推理理论的归结方法，其自动推理理论是真值定义在格蕴涵代数（lattice implication algebra，LIA）结构上格值逻辑系统中的。在已有的确定真值水平α二元归结研究的基础上，作为其继续研究和扩展，引入了基于格值命题逻辑系统LP( X )的非子句多元α-有序线性广义归结方法和演绎，这从本质上避免了一个非子句广义归结演绎到规范子句的形式。随后，得到LP( X )中的非子句多元α-有序线性广义归结演绎是可靠和完备的。该研究工作为格值命题逻辑中基于自动推理的归结提供了一个更有效的方法。