【作者】 李文江；

【导师】 徐扬；

【作者基本信息】 西南交通大学 ， 交通信息工程及控制， 2002， 博士

【摘要】 格是一类重要的代数结构，现实世界中的很多现象都可以用格来刻画，尤其是不可比较性。而建立在格上的格值逻辑系统把已有多值逻辑的链状真值域拓展到较一般的格上，既能处理全序性信息，又能处理非全序性信息，从而更有效地描述人类推理、判断和决策的不确定性。广义模态逻辑属哲学逻辑范畴，对于刻画事物的“势态”、人物的“情态”和过程的“时态”是一种十分有效的工具。本文在格值命题逻辑系统LP(X)和格值一阶逻辑系统LF(X)的基础上，讨论了广义格值模态逻辑系统的语义及语法性质，并对其α-归结原理做了初步探讨，主要在下述三个方面取得了研究成果： 第一部分：关于格值模态命题逻辑系统及其归结方法的研究 在此部分，把模态算子N(必然)和P(可能)引入格值命题逻辑系统LP(X)，建立了新的格值模态命题逻辑系统LMP(X)，并研究了它的语义刻画及语法结构，证明了在此语义解释和语法框架下的系统仍是α-可靠的和协调的；在此基础上，进一步研究了基于格值模态命题逻辑系统LMP(X)的α-归结原理，给出了计算α-直接归结式和α-自归结式的规则，并总结出具体的归结方法。 第二部分：关于格值时态命题逻辑系统及其归结方法的研究 此部分的主要工作是在格值命题逻辑系统LP(X)中引进时态算子E(曾经)、F(将会)及其对偶算子H(曾经总是)、G(将会总是)，提出了以时轴为语境的格值时态命题逻辑系统LTP(X)，并给出其具体的语义解释和语法结构，并讨论了它的一些性质，证明了该系统的可靠性和协调性。此外，研究了与时间有关的(α，t)-归结原理，给出了计算时态归结式的规则，并提出了时态归结的具体方法。 第三部分：关于格值模态一阶逻辑系统及其归结原理的研究 第n页 西南交通大学博士研究生学位论文 这一部分主要是在格值模态命题逻辑系统LMP队）中引进量词和谓词，建立格值模态一阶逻辑系统LMF（广 并给出其语又解释和语法结构，证明了系统的可靠性和协调性；另外，为了判断公式的可满足性，定义了格值模态一阶公式的 Skolem标准型和体解释；在此基础上，对基于系统LMF（）的a一归结原理进行了初步探讨．更多还原

【Abstract】 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).更多还原