Generalized Lattice-Valued Modal Logic System And Resolution Automated Reasoning Based On Lattice Implication Algebra

The lattice is a kind of important algebraic structure. In our life, many phenomena can be described by lattice, especially non-comparability. Lattice-valued logic system based on lattice extends linear valued field of multi-valued logic to lattice, thus not only can deal with order information, but also can deal with non-order information, consequently describe the uncertainty of human reasoning, judging and decision-making more effectively. Generalized modal logic belongs to philosophy logic category. It is a very effective tool to describe the tendency of things, attitude of people and tense of course. Based on lattice-valued propositional logic system LP(X) and lattice-valued first-order logic system LF(X), the author studied semantic and syntax properties of generalized lattice-valued modal logic system, and probed into a - resolution principle. The specific contents are as follows:Part One The Study of Lattice-valued Modal Propositional Logic System and Its Resolution MethodIn this part, we introduced modal operators N(necessary) and P(possible) into lattice-valued propositional logic system LP(X), set up a new lattice-valued modal propositional logic system LMP(X), studied its semantic properties and syntax structure, proved the soundness and consistence of this system. Based on these work, discussed a - resolution principle of lattice-valued modal propositional logic system LMP(X), gave out the rules of computing a - direct resolvent and a - self resolvent, and proposed detailed resolution method.Part Two The Study of Lattice-valued Tense Propositional Logic System and Its Resolution MethodThe main work of this part is to introduce four tense operators E(ever), F(will), H(ever always) and G(will always) into LP(X), put up lattice-valued tense propositional logic system LTP(X) which takes time axis as language circumstance, gave detailed semantic interpretation and syntax structure, and discussed some properties of it, then proved soundness theorem and consistence theorem. Furthermore, studied (a,t)-resolution principle which is related to time, gave some rules of computing tense resolvent, and put forward the method of tense resolution.Part Three The study of Lattice-valued Modal First-order Logic System and Its Resolution PrincipleIn this part, we introduced quantifiers and predicate into LMP(X), put up lattice-valued modal first-order logic system LMF(X), and gave its semantic interpretation and syntax structure, proved soundness theorem and consistence theorem. Moreover, in order to judge the satisfiability of formula, defined Skolem standard type and H-interpretation. Based on these work, made a primary discussion of a - resolution principle based on LMF(X).