Semantic Resolution Automated Reasoning For Linguistic Truth-Valued Lattice-Valued Logic Based On Lattice Implication Algebras

Intelligent information processing based on non-classical logic system is an important research direction of intelligence artificial. It can describe effectively the information with incomparability. In addition, linguistic truth value was usually used to describe the things in the real world when people judge and make a decision for something. So, the intelligent information processing theories and methods based on linguistic truth value is also an important research realm.Based on the previous work on the resolution automated reasoning under classical logic and the resolution automated reasoning under lattice-valued logic, this thesis systematic and intensively investigates the generalized resolution automated reasoning theory, method, algorithm and program in lattice-valued logic, and gets the following research results:Part one:the study on the a-resolvablity of generalized literals in lattice-valued logic system (Ln×L2)P(X).On the framework of lattice-valued propositional logic (Ln×L2)P(X) based on Ln×L2, according to the particular structure of Ln×L2, the a-resolvablities of 0-IESF,1-IESF,2-IESF and other generalized literals are given on the condition that a is a dual molecular.Part two:the study on a-semantic resolution method.The properties of some classes of generalized clauses in lattice-valued logic LP(X) are obtained, and α-semantic resolution methods in LP(X) are established, its soundness and condition completeness are also given. Accordingly, the equivalent transformation between a-semantic resolution in linguistic truth-valued lattice-valued propositional logic Ln(n×2)P(X) and semantic resolution in lattice-valued propositional logic LnP(X) with corresponding truth-valued level is given.a-Semantic resolution methods in lattice-valued first-order logic LF(X) are established, and its soundness and condition completeness are also given. Accordingly, the equivalent transformation between a-semantic resolution in linguistic truth-valued lattice-valued first-order logic Ln(n×2)F(X) and semantic resolution in lattice-valued first-order logic LnF(X) with corresponding truth-valued level is given.Part three:the study on a-generalized semantic resolution method in lattice-valued logic system.a-Generalized semantic resolution methods in LP(X) are established, and its soundness and condition completeness are also given. Accordingly, the equivalent transformation between a-generalized semantic resolution in linguistic truth-valued lattice-valued propositional logic LV(n×2)P(X) and generalized semantic resolution in lattice-valued propositional logic LnP(X) with corresponding truth-valued level is given.a-Generalized semantic resolution methods in lattice-valued first-order logic LF(X) are established, and its soundness and condition completeness are also given. Accordingly, the equivalent transformation between a-generalized semantic resolution in linguistic truth-valued lattice-valued first-order logic LV(n×2)F(X) and generalized semantic resolution in lattice-valued first-order logic LnF(X) with corresponding truth-valued level is given.Part four; the comparability among some resolution methods in lattice-valued logic system.The comparability of a-semantic resolution method with delete strategy and the comparability of a-generalized semantic resolution method with generalized delete strategy in lattice-valued first-order logic LF(X) are obtained. The comparability of a-generalized resolution method with set-support strategy is established, and the soundness theorem and condition completeness theorem of a-generalized set-support resolution in lattice-valued first-order logic LF(X) is given.