节点文献

关于格值逻辑及自动推理的研究

The Study of Lattice-valued Logic and Automated Reasoning

【作者】 李海明

【导师】 徐扬;

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

【摘要】 逻辑学是人工智能研究的重要手段。格是一类重要的代数结构,现实世界中的许多现象都可以用格来刻画,尤其是不可比较性。格值逻辑是一种重要的非经典逻辑,它是经典逻辑和模糊逻辑的推广。格值逻辑把多值逻辑的链型真值域拓广到较一般的格上,既能处理全序信息,又能处理不可比的信息,从而可以更有效地刻画人类的推理、判断和决策的不确定性,尤其是对真值不完全可比较性的研究,能够更真实地刻画人类的思维活动。从逻辑的角度来看,对知识的利用就是推理,就是逻辑演绎。因此,推理不仅是逻辑系统的重要组成部分,也是人工智能领域的核心课题之一。格蕴涵代数是将格与蕴涵代数结合起来的一种代数结构,是研究格值逻辑系统及其性质的一个重要途径。本文的工作是在徐扬教授、秦克云教授等研究成果的基础上,对格蕴涵代数的性质、结构、格值命题逻辑系统中的重言式、自动推理方法、格值命题逻辑系统等进行了一些研究。主要有以下四部分内容组成。 一、代数结构和性质的研究 1、对格蕴涵代数的结构进行了研究,证明了非链的五元格不能构成格蕴涵代数,非链的中界格不能构成格蕴涵代数。 2、讨论了L型广义扩展原理在L型模糊集范畴中的应用。本文给出基于L型模糊关系的L型广义扩张原理,在此基础上通过L型广义扩张原理构造三个模糊集范畴,并讨论了它们之间的相互关系。 二、一类格值逻辑系统中的重言式和逻辑公式的神经网络计算 1、重言式在逻辑系统的应用中起着重要的作用。本文分析讨论了基于格蕴涵代数直积的格值逻辑系统中的α-重言式和F-重言式,作为两个实例,详细讨论了两个格值逻辑系统L4P(X)和L6P(X)中的重言式和F-重言式的结构。 2、提出一种利用神经逻辑单元动态地构造神经网络的算法来对一些逻辑系统中的逻辑公式的真值进行计算。这种方法可以对逻辑公式的原始形态直接进行计算,无需化简。如果进行了化简,则本方法将更有效。本方法可以方便地制作成硬件来实现。第n页.西南交通大学研究生博士学位论文三、自动推理方法的研究 提出了基于路径搜索的自动推理方法,它不同于归结原理,采用直观的路径搜索的方法,建立了相应的自动推理算法,将其应用于二值逻辑、中界格逻辑和六元格蕴涵代数逻辑系统中,证明了这种算法的可靠性和完备性,并分析了这种算法的有效性。四、格值逻辑系统的研究 建立了基于格蕴涵代数的格值命题逻辑系统l试X),并讨论了它的语法和语义问题,证明了可靠性定理。

【Abstract】 Logic is a main tool in the research of artificial intelligence. Lattice is an important kind of algebraic structure. In our life, many phenomena can be described by lattice, especially non-comparability. Lattice-valued logic is an important kind of non-classical logic and an extension of both classical logic and fuzzy logic. It extends linear valuation field of many-valued logic to a more general lattice, thus can deal with both order and non-order information, such as non-comparable information, consequently describe the uncertainty of human reasoning, judging and decision-making more effectively. In the view of logic, reasoning is the use of knowledge and logic deduction. Therefore reasoning is not only the very important part of logic, but also the key aspect in the area of artificial intelligence. Lattice implication algebra is a kind of algebraic structure combined with lattice and implication algebra. It is an important method in the research of lattice-valued logic. Based on the production of other researchers such as professor Xu Yang and professor Qin Keyun, this paper discusses the structure and properties of lattice implication algebra, tautologies in some lattice-valued systems, automated reasoning methods, lattice-valued prepositional logic system. This paper mainly contains following four parts.1. The study of algebraic structure and properties(1) Some properties and structure of lattice implication algebra are discussed. It is proved that lattices with five elements and lattices with an intermediate element can not form lattice implication algebra except they are chains. (2) The applications of L-generalized extension principle in L-fuzzy set theory are studied. The L-generalized extension principle for L-fuzzy set is introduced and some of its properties are discussed. Then three L-fuzzy set categories are defined and their relations are discussed.2. Studies on the tautologies in some lattice valued logic systems andformula computation by means of neural net works.(1) Tautologies play a significant role in logic applications, a- Tautologies and F- Tautologies in some lattice valued logic systems whose truth-value lattice are products of lattice implication algebra are discussed. As examples, a- Tautologies and F- Tautologies in lattice valued logic systems 1-4P (X) and L6P (X) are discussed in detail.(2) A kind of calculus method that is used to determine the truth-values of propositional logic formulae by means of the dynamic neural networks is proposed. It is not necessary that the formulae be simplified into normal form. If the formula is simplified before calculus, then this method will be more effective. The method can be executed mechanically. It can be extended to fuzzy logic systems and some lattice-valued logic systems.3. The study on automated reasoningA new automated reasoning method based on path searching was proposed. It can be used to validate the unsatisfiability and satisfiability of propositional logic formulae quickly. The soundness and completeness of this method are proved. The efficiency of this arithmetic is also discussed. It is applied to classical logic systems and some lattice valued systems.4. Study on lattice-valued logic systemA lattice-valued propositional logic system lp(X) based on lattice implication algebra is proposed. The syntax and semantics of lp(X) are discussed. The soundness theorem is proved.

节点文献中: 

本文链接的文献网络图示:

本文的引文网络