New applications for many-valued theorem proving in various subfields, for example in the theory of error-correcting codes, in non-monotonic reasoning, and in formal software and hardware verification, demand efficient automatic proof procedures for many-valued logics. Many successful theorem-proving methods in two-valued logic, notably resolution, presume the existence of a conjunctive normal form (CNF). We present a general satisfiability preserving transformation of formulae from arbitrary finitely valued logics into a CNF which is based on signed atomic formulae. The transformation is always linear with respect to the length of the input, and we define a generalized concept of polarity in order to avoid the generation of redundant clauses. The transformation rules are based on the concept of‘sets-as-signs’developed earlier by the author in the context of tableau-based deduction in many-valued logics. We discuss several possible resolution rules that operate on the signed CNF including a streamlined version for so-called regular logics, a class of finitely valued logics defined earlier by the author. We compare our work to related approaches to many-valued resolution, and argue that our approach is computationally more effici
展开▼
