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).

Authors

• Xingxing He
• Yang Xu Purdue University
• Jun Liu Carnegie Mellon University
• Da Ruan

Keywords

• Lattice-valued logic
• Lattice implication algebra
• α - Resolution
• α - Lock resolution
• Automated reasoning