On ?-multi-ary Linear Resolution Automated Reasoning Based On Lattice-valued Logic

One of the most challenging aspects of the field of artificial intelligence is automatic reasoning (theorem machine proving). Automatic reasoning based on resolution is an important research realm in automatic reasoning. Its research results have been applied to many important areas, such as artificial intelligence, logic programming, problem solving,software model checking and testing, security protocols, automatic program verification,question answering systems etc. There exists some problems produce incomparability because of its multi-factors. The problems with incomparable information are often complicated. Automatic reasoning of lattice-valued logic system based on lattice implication algebra is one of the efficient approaches to solve such problems.Based on the research work of other scholars, combining with resolution reasoning methods based on classical logic, the ? - multi-ary linear resolution in lattice-valued logical system based on lattice implication algebras is researched in details including its theory,methods, algorithms and programs. The main achievements of the research are as follows:Part 1, all possible forms of a class of generalized literals be 3-order indecomposable extremely simple form in lattice-valued propositional logic LnP(X) based on Lukasiewicz implication algebra Ln are obtained. For one of the particularly important 3-IESF, the determination of ? - resolution between it and n-IESF (0?n?3) is given.Part 2, based on ?-multi-ary resolution principle in lattice-valued logical system, the determinations of ? - resolution of any 3-ary generalized literals among boundary generalized literals of all categories of generalized literals and some properties of? - resolution fields in lattice-valued logical system are gotten.Part 3, based on ? - multi-ary resolution principle in lattice-valued propositional logical system LP(X), ? - multi-ary minimal resolution principle based on lattice-valued propositional logical system LP(X) is proposed. Its soundness and completeness are established. Then, based on ?-multi-ary minimal resolution principle, ? - multi-ary ordered linear minimal resolution method in LP(X) is given. Its soundness and conditional completeness are established, and the efficiency of ?-multi-ary ordered linear minimal resolution method in LP(X) is analyzed. Furthermore, the ?-multi-ary ordered linear minimal resolution algorithms based on lattice-valued propositional logical system LP(X)are constructed. In order to improve the efficiency of the algorithm, the method of preprocessing the generalized clause set and six strategies for selecting and judging generalized literals are given. Its soundness and completeness are proved. The time complexity of algorithms are analyzed. An example is given to illustrate the effectiveness of the algorithm. Meanwhile,the ?-multi-ary ordered linear minimal resolution automated reasoning program based on LP(X) is designed.Part 4, in lattice-valued first-order logical system LF(X), ? - multi-ary minimal resolution principle is proposed, a lifting lemma is established, its soundness and completeness are proved, and equivalent transformation theory of ?-multi-ary minimal resolution principle in LF(X) are obtained. Then, based on ? - multi-ary minimal resolution principle, ?-multi-ary ordered linear minimal resolution method in LF(X) is given, its soundness and conditional completeness are established, equivalent transformation theory of?-multi-ary ordered linear minimal resolution method in LF(X) are obtained, and the efficiency of ? - multi-ary ordered linear minimal resolution method in LF(X) is analyzed.Furthermore, the ? - multi-ary ordered linear minimal resolution algorithm based on lattice-valued first-order logical system LF(X) is constructed, its soundness and completeness are given, the time complexity of algorithms are analyzed, and an example is given to illustrate the effectiveness of the algorithm in LF(X).Part 5, in order to further improve the ability and efficiency of resolution automated reasoning and to further enhance ?-multi-ary minimal resolution for generalized literals,non-clausal ?-multi-ary minimal generalized resolution principle based on lattice-valued propositional logical system LP(X) is proposed. Then, the soundness and completeness of the generalized resolution principle are proved. Non-clausal ?-multi-ary ordered linear generalized resolution method in LP(X) is given. Its soundness and conditional completeness are got. Also, the non-clausal ?-multi-ary ordered linear generalized resolution algorithm in LP(X) is constructed. Further, the non-clausal ? - multi-ary minimal generalized resolution principle based on LP(X) is extended to the corresponding in LF(X), non-clausal?-multi-ary minimal generalized resolution principle based on LF(X) is proposed, its lifting lemma and equivalent transformation theory of are obtained, and its soundness and completeness are established. Then, non-clausal ?-multi-ary ordered linear generalized resolution method in LF(X) is given. Its soundness and conditional completeness are established. The non-clausal ?-multi-ary ordered linear generalized resolution algorithm based on in LF(X) is constructed.