α-Lockα-Lock resolution method for a lattice-valued first-order logic

This paper focuses on resolution-based automated reasoning approaches in a lattice-valued first-order logic LF(X  ) with truth-values defined in a logical algebraic structure—lattice implication algebra (LIA), which aims at providing the logic foundation to represent and handle both imprecision and incomparability. In order to improve the efficiency of α-resolutionα-resolution approach proposed for LF(X  ), firstly the concepts of α-lockα-lock resolution principle and deduction are introduced for lattice-valued propositional logic LP(X) based on LIA, along with its soundness and weak completeness theorems. Then all the results are extended into LF(X  ) by using Lifting Lemma. Finally an α-lockα-lock resolution automated reasoning algorithm in LF(X) is proposed for the implementation purpose. This work provides a theoretical foundation for more efficient resolution-based automated reasoning algorithm in lattice-valued logic LF(X).

► We present the α-lockα-lock resolution method and deduction for LF(X  ) based on LIA.
► We establish its soundness and weak completeness theorems by using Lifting Lemma.
► We contrive an α-lockα-lock resolution automated reasoning algorithm.
► We provide a theoretical foundation for resolution-based automated reasoning in LF(X).
► We provide the logic foundation to represent and handle incomparability.