α-Generalized lock resolution method in linguistic truth-valued lattice-valued logic

Abstract

This paper focuses on effcient non-clausal resolution-based automated reasoning methods and algorithms for a lattice-ordered linguistic truth-valued logic, which corresponds to extensions of α-lock resolution. Firstly, α-generalized lock resolution is proposed for lattice-valued propositional logic and first order logic, respectively, along with their concepts, soundness and completeness. Then, α-generalized lock resolution for first order linguistic truth-valued lattice-valued logic F(X) is equivalently transformed into that for propositional logic P(X), which can greatly reduce the complexity of the resolution procedure. Finally, α-generalized linear semi-lock resolution is discussed, and its general algorithm is also contrived. This work provides more efficient and natural resolution automated reasoning scheme in linguistic truth-valued logic based on lattice implication algebra with the aim at establishing formal tools for symbolic natural language processing.

Keywords

• Non-clausal resolution
• α-Generalized lock resolution
• α-Generalized linear semi-lock resolution
• Linguistic truth-valued lattice-valued logic
• Lattice implication algebras