α -ORDERED LINEAR MINIMAL RESOLUTION METHOD IN LATTICE-VALUED PROPOSITIONAL LOGIC SYSTEM LP(X)

摘要

Based on the academic ideas of resolution-based automated reasoning and the previously established research work on general form of α-resolution based automated reasoning schemes in the framework of lattice-valued logic with truth-values in a lattice algebraic structure-lattice implication algebras (LIA), this paper is focused on investigating α-n(t)-ary resolution dynamic automated reasoning method in lattice-valued prepositional logic LP(X) based in LIA. In this paper, the definition of α-ordered linear minimal resolution in LP(X) is introduced firstly. Then, its soundness and completeness are proved. One of key issues for α-n(t)-ary resolution dynamic automated reasoning for LP(X) is how to choose generalized literals. It will guide how to choose generalized literals to improve the resolution efficiency in LP(X). This lays the foundation for the further study on α-n(t)-ary resolution automated reasoning.