Research On Automated Reasoning Of Lattice-valued Logic Based On Lattice Implication Algebra

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.