α-Minimal Resolution Principle For A Lattice-Valued Logic

• Main Authors: Hairui Jia, Yang Xu, Yi Liu, Jun Liu
• Format: Article
• Language: English
• Published: Atlantis Press 2015-01-01
• Series: International Journal of Computational Intelligence Systems
• Subjects: Automated reasoning; lattice-valued propositional logic LP(X); lattice-valued first-order logic LF(X); α-minimal resolution principle; α-minimal resolution group
• Online Access: https://www.atlantis-press.com/article/25868575.pdf

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.