【作者】 孟丹；

【导师】 徐扬；

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

【摘要】 关于不确定性信息处理的研究是当前人工智能领域的一类重要的研究内容。为了处理不确定性信息，人们发展了各种相关的工具和方法，也形成了大量相关的研究成果。其中多值逻辑对于刻画和处理客观世界中的不确定性或者人类主观认识客观世界过程中所产生的不确定性起到了重要的作用。格值逻辑是一种重要的多值逻辑，它特别将链状真值域扩充为较一般的格结构，既能处理全序信息，又能处理不可比信息，从而可以更有效地描述和处理人类推理、判断和决策中的某种不确定性。 基于归结方法的自动推理是定理机器证明中重要的手段之一。自从1965年，基于归结方法的自动推理提出以来，关于归结原理的研究取得了许多研究成果并在人工智能，逻辑编程，定理证明，问题求解和数据库理论等领域中得到了广泛应用。 为处理基于某些不确定性信息的推理问题，建立在多值逻辑系统中的归结理论与方法的研究得到了快速发展。本文的研究工作即属于多值逻辑中的归结理论与方法研究的范畴。本文的工作是在徐扬和秦克云教授等关于格蕴涵代数和格值逻辑系统的研究成果基础上，对基本而重要的格值命题系统LP（X）和一阶逻辑系统LF（X）中基于归结原理的自动推理方法以及相应的归结算法实现的相关问题进行了研究，并取得了如下主要成果： 一．经典命题逻辑系统上基于数值矩阵运算的归结算法的研究 提出了基于数值矩阵运算的归结算法，并证明了该算法的可靠性和完备性。在该算法中，首先把逻辑公式对应的子句集表示成数值矩阵的形式，然后通过矩阵行之间的运算得出对应的公式是否为可满足的结论。为提高该算法的效率，提出了对该算法的改进算法——基于数值矩阵的线性归结算法。 二．四元非链的格值命题逻辑系统L₄P（X）中的归结原理及算法的研究 将经典逻辑系统上矩阵运算归结算法的思想扩展到基于四元非链的格蕴涵代数的格值命题逻辑系统L₄P（X）中。首先考虑了L₄P（X）上的归结原理，证明了归结原理的可靠性和完备性，然后在归结原理的基础上提出了L₄P（X）中的矩阵归结算法。 三．六元非链的格值命题逻辑系统L₆P（X）中的归结原理及算法的研究 1．考虑了化格值命题逻辑公式为准广义合取范式的问题，得出了公式准广义合取范式的存在性以及化格值命题逻辑公式为准广义合取范式的算法，这足使用计算机实现归结所必须解决的首要问题；第ii页西南交通大学研究生博士学位论文 2.提出了格值命题逻辑系统中基于超滤的归结原理，由于格值逻辑系统的 真值域是格蕴涵代数，而超滤作为格蕴涵代数的特殊子集合，可以作为 对格值逻辑公式的分类标准; 3.考虑了六元非链的格值命题逻辑L6尸（X）的基于超滤的归结原理，以 及归结原理的可靠性，适用性等，并得出了该归结原理的可靠性和弱完 备性定理;同时为使得基于超滤的归结原理可以处理更多的格值逻辑公 式的可满足性判断问题，提出了归结删除原理以及序归结的放缩原理归 结方法。四.六元非链的格值一阶逻辑系统L6F（X）的归结原理及算法的研究 1.考虑了化格值一阶逻辑公式为可归约形式的问题，得到了任一格值一阶 逻辑公式的可归约形式的存在性以及化格值一阶逻辑公式为可归约形 式算法的计算机实现; 2.提出了六元格值一阶逻辑系统L6F（X）的基于超滤水平进行归结的归 结原理，证明了公式的可满足性与H二6:aod域上公式的可满足性的同 可满足性; 3‘同时证明了归结原理的可靠性定理以及弱完备性定理; 4.为判断更多L6F（X）中公式的可满足性问题，提出了基于超滤的归结 删除原理以及序归结的放缩原理。关键词:人工智能，自动推理，归结原理，格蕴涵代数，格值逻辑系统更多还原

【Abstract】 Research on uncertainty information processing is an important field in artificial intelligence. There are a lot of related theoretical and applicable research results in order to deal with uncertainty information. Multiple-valued logic takes a great effect when human describe or deal with uncertainty information. Fuzziness and imcornpara-bility are two kinds of uncertainty often associated with haman’s intelligent activities in the real world, and they exist not only in the processed object itself, but also in the course of the object being dealt with. Lattice-valued logic is one of important multivalued logics. It extends the truth filed to general lattice. And it can deal with not only linear information but also incomparable information. So it, can describe or deal with uncertainty information more suitably.Automated reasoning based on resolution is an important method in automated theorem proving(ATP). It has been extensively studied and made great progress since its introduction in 1965. It has been applied to artificial intelligence, logic programming, theorem proving, question solving and database theory.etc.Research on resolution on multi-valued logic has been given great attention and made great improvement in order to deal with reasoning on uncertainty information. Research in this paper belongs to resolution on multi-valued logic. It is based on lattice implication alagbra and lattice-valued logic system given by Yang Xu and Keyun Qin. Resolution principle and method and corresponding algorithm are focused in this paper. Some fundamental lattice-valued proposition logic system LP(X) and first-order logic system LF(X) are focused. The following research results are achieved.1. Research on Numeric Matrix Resolution Algorithm on Classical Propositional Logic systemResolution algorithm of numeric matrix operation is discussed. And its soundness and completeness are proved. In this algorithm, present clasue set of a formula to a numeric matrix first, then operate on numeric matrix and come to the conclusion if the formula is satisfiable. Based on it, linear resolution algorithm is given as an improvement of matrix resolution.2. Research on Resolution on Four-valued Non-chain Type Lattice-valued Propositional Logic L4P{X)Numeric matrix resolution algorithm on classical logic system are extended to four-valued non-chain type lattice-valued propostion logic system L4P(X) based on lattice implication algebra. Resolution principle and itssoundness theorem and completeness theorem on L4P(X) are considered. Some transformations which preserve the satisfiability are given in order to improve efficiency of resolution.3. Research on Resolution on Six-valued Non-chain Type Lattice-valued Logic L6P(X)(a) The problem of transforming a lattice-valued propostion logic formula to a quasi-generalized conjunction normal form is considered. Algorithm of transforming any formula in LP(X) to quasi-generalized conjunction normal form is proved. It is the ultimate step for resolution on computer.(b) Resolution principle by using ultrafilter in LP(X) is considered.(c) Resolution principle based on L6P{X) by using ultrafilter is considered. Soundness theorem and quasi-completeness theorem are proved in this section. Resolution and elemination principle and order-resolution method are presented in order to judge more formulae in L6P(X).4. Research on Resolution on Six-valued Non-chain Type Lattice-valued First-order Logic L6F(X)(a) Algorithm of transforming any formula in LF{X) to a reducible form is given. It is necessary and important for resolution on computer;(b) Resolution principle by using ultrafilter in L6F(X) is given and satisfiability of formula and its same satisfiability in Herbrand field is proved.(c) Soundness theorem and quasi-completeness theorem of resolution principle by using ultrafilter in L6P(X) are proved .(d) Resolution elimination principle is considered in order to judge more formulae.更多还原