α-Minimal Resolution Principle For A Lattice-Valued Logic

Abstract

Based on the academic ideas of resolution-based automated reasoning and the previously established research work on binary α-resolution based automated reasoning schemes in the framework of lattice-valued logic with truth-values in a lattice algebraic structure-lattice implication algebra (LIA), this paper is focused on investigating α-n(t)-ary resolution based dynamic automated reasoning system based on lattice-valued logic based in LIA. One of key issues for α-n(t)-ary resolution dynamic automated reasoning is how to choose generalized literals in each resolution. In this paper, the definition of α-minimal resolution principle which determines how to choose generalized literals in LP(X) is introduced firstly, as well as its soundness and completeness being proved. α-minimal resolution principle is then further established in the corresponding lattice-valued first-order logic LF(X) along with its soundness theorem, lifting lemma and completeness theorem. These results lay the theoretical foundation for research of α-n(t)-ary resolution dynamic automated reasoning.

Keywords

• Automated reasoning
• lattice-valued propositional logic LP(X)
• lattice-valued first-order logic LF(X)
• α-minimal resolution principle
• α-minimal resolution group