关键词: 格蕴涵代数, 自动推理, 格值命题逻辑, 非子句多元&alpha, -有序线性广义归结

Abstract: 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 established 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.

Key words: lattice implication algebra, automated reasoning, lattice-valued propositional logic, non-clausal multiary α-ordered linear generalized resolution