\(\alpha\)-resolution principle based on lattice-valued propositional logic \(\text{LP} (X)\) (Q5946276)

The authors of this article consider a system of many-valued reasoning they have worked on since 1990. It is lattice-valued propositional logic \(LP(X)\) having as algebraic counterpart lattice implication algebra. A lattice implication algebra is a special case of a Wajsberg algebra \((A,\neg,\to,1)\), where the set of truth values \(A\) is a bounded lattice, negation \(\neg\) is involution and implication \(\to\) is distributive relative to meet and join in the lattice \(A\). The \(\alpha\)-resolution principle the authors essentially deal with is simply a variant of many-valued binary resolution widely discussed in literature. Using the rule of \(\alpha\)-resolution, one can cut a pair of clauses whose conjunction, speaking informally, is less than some \(\alpha\) in the lattice of truth values. This rule gives rise to the notion of \(\alpha\)-refutation, i.e. a deduction by \(\alpha\)-resolution that ends with the empty clause. The authors state that their resolution rule modification can be applied to checking the consistency of sets of clauses under uncertainity conditions. This resolution has an interesting feature: for some truth value \(\alpha\) one can deduce the empty clause, but for another value, not comparable to \(\alpha\), the empty clause may not be deduced. In other words, the lattice structure of the set of truth values of \(LP(X)\) provides a logic with incomparable objects. The main disadvantage of this article is that some notions used in the proofs of soundness and completeness are not defined. So in order to check the correctness of the proofs the reader should consult earlier works, e.g. \textit{Y. Xu} and \textit{K. Qin}, ``Lattice-valued propositional logic. I'' [J. Southwest Jiaotong Univ., Engl. Version 1, No. 2, 123-128 (1993; Zbl 0807.03020)].