基于格蕴涵代数的格值命题逻辑系统能定性地刻画不可比较性和不精确性.广义文字是该系统中α-归结自动推理的核心概念,是α-归结中的最基本单元.公式的正规性是α-归结原理中保持完备性的重要条件,其语义性质是公式形式的重要反映.从语义角度研究了广义文字的正规性,给出了两种典型正规公式F1→F2和(F1→F2)’的真值情况.为讨论广义文字的形式及其α-可归结性提供了理论基础.%Lattice-valued prepositional logic based on lattice implication algebra can represent incomparability and imprecise. Generalized literal is a core concept of a-resolution principle in this logic system, and it is the basic unit in a-resolution. The normal property of logical formulae is one of important properties in a-resolution automated reasoning for persevering completeness, its semantic properties are characterized by syntactic of logical formulae. In this paper, some normal properties of generalized literals in LP (X) are studied from a semantic view. Concretely, whether the truth values of two traditional types of formulae (I.e., Fi → F2, (Fi→ F2)') are normal is discussed. It provides a theoretical foundation for studying the forms of generalized literals and it's a-resolution fields.
展开▼
