The Study Of Reasoning Method Based On α-Resolution Principle In Lattice-valued Propositional Logic LP(X)

Based on the outcome of Xu Yang and Qin Keyun about lattice implication algebra and lattice-valued prepositional logic LP(X) with truth-value in a lattice implication algebra, the author studied the properties of lattice implication algebra and the α-automated reasoning method based on α-resolution principle of LP(X). The specific contents are as follows:The Study of Lattice Implication AlgebraOn the basis of previous results of lattice implication algebra, this part consists of the following three points:1. Some properties of lattice implication algebra L were discussed, and some important results were given if L was a complete lattice implication algebra.2. The properties of left idempotent elements of lattice implication algebras were discussed, and the conclusion that lattice implication algebra L was equals of the directed sum of the range and dual kernel of a left map constructed by a left idempotent element was proved.3. The properties of the filters of lattice implication algebra were discussed, the theorem was shown that they satisfy the hypothetical syllogism and substitute theorem of the propositional logic.4. The concept of weak niters of lattice implication algebras and their properties and structures are discussed. It is proved that all weak filters of a lattice implication algebra form a topology and the the implication isomorphism betweem two lattice implication algebras is a topological mapping between their topological spaces.The Study of α-automated reasoning method based on the lattice-valued propositional logic LP(X)In this part, the author given an a-automated reasoning method based on the lattice-valued propositional logic LP(X). The soundness and completeness theorem of this method were proved at last. This part consists of the following points:1. The properties of the indecomposable extremely simple form of LP(X) were discussed, the theorem shown that every logical formula of LP(X) was equals of a generalized conjunction (disjunction) normal form.2. The method for judging a logical formula is a indecomposable extremely simpleform or not was discussed, the necessary and sufficient conditions of a logical formula with not more than three implicative connective being a indecomposable extremely simple form was given.3. The α-resolution fields of the indecomposable extremely simple form of LP(X) were discussed, some elementary results were obtained.4. The automated reasoning method based on the resolution principle of classical logic was discussed, the author given a method to describe the set of clauses by using a matrix, and translated the resolution of two clauses to column operations of this matrix. The unsatisfiability of a set of clauses could be judged by using the column operations of this matrix. The soundness and completeness theorem of this method were proved at last.5. The a-automated reasoning method based on the a-resolution principle of LP(X) was discussed, the author given a method to describe the set of simple generalized clauses (veriables and non-subregular 1 - IBSFs are only contained) by using a matrix, and translated the a-resolution of two clauses to column operations of this matrix. The a-unsatisfiability of a set of clauses could be judged by using the column operations of this matrix. The completeness theorem of this method were proved at last.