CADE-18 tutorial
July 25th, 2002

Classical Gentzen-type Methods in Propositional Many-Valued Logics

The problem of adapting to many-valued logics the usual methods of automated reasoning (like Gentzen-type systems, tableaux, and resolution) has attracted a lot of attention in recent years. (especially because of the wide range of applications that many-valued logics have found in Computer Science). The main idea which is used in most of the works on this subject is to use for any particular n some n-valued counterparts of the structures used in the usual proof systems for classical logic (like sequents with n components, tableaux systems with n signs, etc.). This fact is well reflected in two recent survey papers In the Handbook of Automated Reasoning and the Handbook of Tableaux Methods. In this tutorial we will concentrate, in contrast, on proofs systems which use the same syntactic structures as the classical ones (with particular emphasis on Gentzen-type systems, on which all other systems are based). This approach has two advantages. First, the implementation of the proofs systems described here can be based on existing systems, because no new data structure is used. Second, two sided sequents (like those used in classical logic) can directly represent the consequence relation of any given logic, and this is, after all, what logics are all about.

A decent Gentzen-type system for a logic should allow for direct proofs, which means that it should admit some useful forms of cut elimination and the subformula property. In the tutorial we shall explain the main difficulty in developing classical Gentzen-type systems with these properties for many-valued logics, and discuss the possible methods of overcoming this difficulty. We then illustrate with numerous examples these methods. Our examples include practically all 3-valued and 4-valued logics, as well as Goedel finite-valued logics and several well-known infinite-valued logics which can be taken to be semi-finite.

One of our main goals is to demonstrate the strong connection which exists in all cases between semantic completeness (usually a strong one) and (a strong version of) the admissibility of the cut rule. The various proofs we present (most of which are new) establish therefore both strong completeness and strong cut-elimination at the same time.

Finally, we show how to use the systems we present as a basis for applying the methods of resolution and of tableaux for many-valued logics. The way this is done is very similar to that in the classical, two-valued case.


Arnon Avron <>, Tel Aviv U, Israel