© 1994 by Oxford University Press
Original Articles |
Short Conjunctive Normal Forms in Finitely Valued Logics
Institut für Logik, Komplexität und Deduktionssysteme, Fakultät für Informatik, Universität Karlsruhe 76128 Karlsruhe, Germany. E-mail:haehnle{at}ira.uka.de
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 efficient.
Keywords: Clausal normal form; many-valued logic; semantic tableaux; resolution; polarity