| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 381241 | Engineering Applications of Artificial Intelligence | 2011 | 7 Pages |
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.
