Generalized Modal Logic And Resolution Automated Reasoning Based On Linguistic Truth-valued Lattice Implication Algebra

The rapid improvement of artificial intelligence technology is inseparable from the development of logic.For different problems,different logic systems are constructed.Due to the constant change of things,the truth values of propositions depend on time,space and other influential factors,and modal logic is a powerful tool to deal with this problem.Lattice-valued modal logic with lattice implication algebra as the true value domain can deal with not only totally ordered information,but also non-totally ordered information.In daily life,people usually use natural language to express.In order to better apply lattice-valued modal logic in practice,this thesis proposes a 6-element linguistic truth-valued modal propositional logic system and a 6-element linguistic truth-valued modal first-order logic system with 6-element linguistic truth-valued lattice implication algebra as the true value domain.The semantic theory,grammatical structure and resolution principles of the logic systems are studied.The main research results are shown as follows:1.Based on 6-element linguistic truth-valued lattice implication algebra and lattice-valued modal propositional logic system,the semantic representation of 6-element linguistic truth-valued modal propositional logic system is proposed.An evaluation map that maps the set of 6-element linguistic truth-valued modal propositional logic formulas and the set of possible worlds to 6-element linguistic truth-valued lattice implication algebra is defined,and its operations and properties are analyzed.This thesis studies the J-strong complementary literal,J-general complementary literal and J-weak complementary literal based on filter J,and proposes strong resolution formula,general resolution formula and weak resolution formula based on filter J.The J-resolution principle of this system is discussed.The theorems of both soundness and completeness of this J-resolution principle are proved,and the ?-resolution method is proposed.This thesis studies the ?-strong complementary literal,?-general complementary literal and ?-weak complementary literal based on ?,and proposes strong resolution formula,general resolution formula and weak resolution formula based on ?.The ?-resolution principle of this system is discussed.The theorems of both soundness and completeness of this ?-resolution principle are proved,and the ?-resolution method is proposed.The validity of the J-resolution method and the ?-resolution method is illustrated by two examples.Through the analysis of the resolution field,the relationship between J-resolution and ?-resolution is summarized.2.6-element linguistic truth-valued modal first-order logic system is proposed by introducing the predicate and quantifier into the 6-element linguistic truth-valued modal propositional logic system.An evaluation map that maps the set of 6-element linguistic truth-valued modal first-order logic formulas and the set of possible worlds to 6-element linguistic truth-valued lattice implication algebra is defined,and its operations and properties are analyzed.By defining the modal degree of 6-element linguistic truth-valued modal first-order logic formula,a method to convert the 6-element linguistic truth-valued modal first-order logic formulas into the generalized Skolem standard form is given,and the?-resolution principle of the system is proposed.It provides a new theoretical preparation for the establishment of a resolution method based on linguistic truth-valued modal logic system.