The Study Of Lattice-valued Logic And Automated Reasoning

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.