On the refutational completeness of signed binary resolution and hyperresolution (Q1037933)

This article addresses the problem of refutational completeness of signed binary resolution and hyperresolution in many-valued logic. The main results of the paper can be summarized as follows: 1. After introducing the resolution calculi studied in the paper, the author shows that one of the rules of the calculus (namely the merging rule) is redundant. 2. Refutational completeness of signed resolution is studied. {\parindent=6mm \begin{itemize}\item[(a)] It is proved that refutational completeness is guaranteed provided that the sets of signs which appear in any subset of the clauses under consideration satisfy the ``finitary disjunction condition'' (the ``finitary disjunction condition'' holds for a family of sets \(X\) if for all \(Y \subseteq X\) such that \(\bigcap Y = \emptyset\) there exists a finite subset \(Y_f\) of \(Y\) with \(\bigcap Y_f = \emptyset\)). \item[(b)] It is shown that the additional restriction is essential. An example of a countable clausal theory is given which is unsatisfiable and for which no refutations by signed binary resolution (or hyperresolution) exist. \end{itemize}} 3. The satisfiability problem in many-valued logics is studied (both for finite and for infinite sets of truth values). A signed DPLL procedure is then introduced (which is sound and complete for finite sets of clauses and finite sets of truth values).