On compatibilities of ?-lock resolution method in linguistic truth-valued lattice-valued logic
The paper focuses on the efficient resolution-based automated reasoning theory, approach and algorithm for a lattice-ordered linguistic truth-valued logic. Firstly two hybrid resolution methods in linguistic truth-valued lattice-valued logic are proposed by combining ?-lock resolution with generalized deleting strategy and ?-linear resolution. ?-Lock resolution for first-order linguistic truth-valued lattice-valued logic \(\fancyscript{L}_{V(n \times 2)}F(X)\) is equivalently transformed into that for propositional logic \(L_{n}P(X)\) which reduce much the complexity of the resolution procedure. Then the compatibilities of ?-lock resolution with generalized deleting strategy and ?-linear resolution are discussed. We finally contrive an algorithm for ?-linear semi-lock resolution and some examples are provided to illustrate the proposed theory and algorithm. This work provides effective support for automated reasoning scheme in linguistic truth-valued logic based on lattice-valued algebra with the aim at establishing formal tools for symbolic natural language processing.
compatibilities ?-lock resolution linguistic truth-valued lattice-valued logic generalized deleting strategy ?-linear resolution ?-linear semi-lock resolution