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 \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\fancyscript{L}_{V(n \times 2)}F(X)$$\end{document} is equivalently transformed into that for propositional logic \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$L_{n}P(X)$$\end{document} 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.