On Multi-Ary α-Sematic Resolution Automated Reasoning Based On Lattice-Valued Logic

Automatic reasoning (theorem machine proving), has been an important field of artificial intelligence research. Automatic reasoning based on resolution is one of effective methods for "theorem machine proving". The research results can be widely used in natural language understanding, problem solving, automatic program design and program verification etc. There exists a kind of typical uncertainty—incomparability, the problems with incomparable information are often complicated. Lattice-valued logic based on lattice implication algebras can characterize the comparable and incomparable information.The dissertation mainly focuses on substructures of lattice implication algebras and resolution automated reasoning in lattice-valued logical system based on lattice implication algebras. The filter theory and congruence theory are studied thoroughly and systematically; the structures of a-resolution fields in lattice-valued logical system based on lattice implication algebras are investigated; drawing lessons from semantic resolution automated reasoning methods based on classical logic, the multi-ary α-semantic resolution is discussed in details including its methods, algorithms and program based on multi-ary α-resolution principle in lattice-valued logical systems. Concretely, the contents of the dissertation include the following aspects:Part 1, Fuzzy filter theory and fuzzy congruence theory of lattice implication algebras are studied in details. Firstly, the concepts of minimal prime filter, fuzzy prime filter, LT-fuzzy filter based on t-norm T on a lattice and interval-valued T-fuzzy filter based on interval-valued t-norm T are introduced in lattice implication algebras; the properties、 structures and equivalent characterizations of minimal prime filter are given respectively; Some properties and equivalent characterizations of LT-filters are obtained; the properties of interval-valued T-fuzzy filters are given, and some kinds of interval-valued T-fuzzy filter are introduced and the relations among them are also investigated. Secondly, the Fuzzy congruence theory, LT-fuzzy congruence theory based on t-norm T on a lattice, interval-valued T-fuzzy congruence theory based on interval-valued t-norm T in lattice implication algebras are established respectively; the properties of these fuzzy congruence relations are characterizated; the quotient lattice implication algebras induced by these fuzzy congruence relations and homomorphism theorems are obtained respectively. These lay the foundation for researching the structure of α-resolution field of generalized literals in lattice-valued logical systems.Part 2, The structures of a-resolution fields in lattice-valued logical system based on lattice implication algebras are investigated. The algebraic structure of α-resolution fields in lattice-valued logics are obtained. The determinations of α-resolution of any 3-ary generalized literals whose number of implication operators not more than 2 in lattice-valued logic are given. These lay the foundation for researching multi-ary α-resolution methods based on lattice-valued logical systems.Part 3, The relative theories of multi-ary α-resolution principle based on lattice-valued propositional logical system LP(X) are further investigated, the basic principle of the number of generalized literals which take part in the multi-ary α-resolution vary with the resolution deduction in LP(X); the algebraic structures of the set of multi-ary α-resolvents in LP(X) are obtained; the validities of multi-ary α-resolution principle in LP(X) are analyzed, which will lay the theoretical foundation for the multi-ary α-semantic resolution method in LP(X). The multi-ary α-semantic resolution method based on lattice-valued propositional logical systems LP(X) is established, its soundness and conditional completeness are given, the efficiency of multi-ary α-semantic resolution method is analyzed; the multi-ary α-semantic resolution algorithms based on lattice-valued propositional logical systems LP(X) is constructed, its soundness and completeness are given, and an example is given to illustrate the correctness of the proposed algorithm, meanwhile, the validity and complexity of this algorithms are analyzed; the multi-ary α-semantic resolution automated reasoning program based on LP(X) is designed.Part 4, The relative theories of multi-ary α-resolution principle based on lattice-valued first-order logical system LF(X) are further investigated, the basic principle of the number of generalized literals which take part in the multi-ary α-resolution vary with the resolution deduction in LF(X); the descent lemma and equivalent transformation theory of multi-ary α-resolution in LF(X) are obtained; the validities of multi-ary α-resolution principle in LF(X) are analyzed, which will lay the theoretical foundation for the multi-ary α-semantic resolution method in LF(X). The multi-ary α-semantic resolution method based on lattice-valued first-order logical systems LF(X) is established,its soundness and conditional completeness are given, the efficiency of multi-ary α-semantic resolution method are analyzed; the multi-ary α-semantic resolution algorithms based on lattice-valued first order logical systems LF(X) is established, its soundness and completeness are given, and an example is given to illustrate the validity of the proposed algorithm.