Classical Resolution for Many-Valued Logics

We present a resolution-based proof method for finite-valued propositional logics based on an algorithmic reduction procedure that expresses these logics in terms of bivalent semantics. Our approach is hybrid in using some elements which are internal and others which are external to the many-valued logic under consideration, as we embed its original language into a more expressive metalanguage to deal with the satisfiability problem. In contrast to previous approaches to the same problem, our target language is fully classical, what turns the design of the resolution-based rules for a specific many-valued logic into a straightforward task. Correctness results, which are proved in detail in the present study, follow easily from results on classical resolution. We illustrate the application of the method with examples, and comment on its implementation, readily achievable by direct translation into classical propositional logic, making use of reliable existing automated provers.