\(\alpha\)-resolution principle based on first-order lattice-valued logic \(\text{LF}(X)\) (Q5946327)

This article is a continuation of the authors' previous work ``\(\alpha\)-resolution principle based on lattice-valued propositional logic \(\text{LP}(X)\)'' [Inf. Sci. 130, No. 1-4, 195-223 (2000; Zbl 0987.03010)], where they considered many-valued logics of the special kind with partially ordered sets of truth-values. In the present article, a resolution calculus for the corresponding first-order many-valued logic is developed. The authors use the notion of \(\alpha\)-resolution, i.e., resolution relative to some truth-value \(\alpha\) in the lattice of truth values. A variety of notions corresponding to the notions of classical resolution are defined. The authors' work has an emphasis on such lattice implication algebras that do not satisfy the axioms of Boolean algebra. These algebras are called proper lattice implication algebras. The main result is Theorem 3.6 giving the completeness of the \(\alpha\)-resolution principle. The proof of this theorem is rather sketchy and is based on the completeness theorem 3.4 from the previous paper cited above. The thing that confused me a bit in this paper was the definition of the complementation \('\). If we followed the authors' definition of \('\) as ``an order-reversing involution'' we could come to the conclusion that this paper deals only with algebras having linearly ordered sets of truth values, since an involution cannot be uniquely defined on a partially ordered set which is not linearly ordered. But from the context of the paper it becomes clear that the \('\) operation is a complementation and we can define it equivalently as \(x'=x\to 0\). So, the authors' results remain consistent if we think of the \('\) operation as a complementation rather than an involution.