On the refutational completeness of signed binary resolution and hyperresolution

Signed binary resolution and hyperresolution belong to the basic resolution proof methods. Both the resolution methods are refutation sound and, under some finitary restrictions, refutation complete. Our aim is to investigate their refutational completeness in a more general case. We shall assume that clausal theories may be countable sets and the set of truth values an arbitrary one. There are unsatisfiable countable clausal theories for which there do not exist refutations by signed binary resolution and hyperresolution. We propose a criterion on the existence of a refutation of an unsatisfiable countable clausal theory by the investigated resolution methods. Two important applications of the achieved results to automated deduction in signed logic: Herbrand's theorem and a signed Davis–Putnam–Logemann–Loveland (DPLL) procedure will be discussed.