Article ID Journal Published Year Pages File Type
390209 Fuzzy Sets and Systems 2009 15 Pages PDF
Abstract

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.

Related Topics
Physical Sciences and Engineering Computer Science Artificial Intelligence