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 approach proposed for LF(X), firstly the concepts of α - 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 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).