More and more computer science applications demand the extension of classical logic with its bivalent (two-valued) semantics to “many-valued” logics that provide larger sets of truth values. Among these, the class of finite-valued logics can still be characterized by truth tables, but decision procedures based on truth-table computation are inefficient compared to the methods based on analytic tableaux known for classical logic. The present paper thus investigates tableau-based deduction methods for finite-valued logics.

The core idea is that any compositional finite-valued logic can also be characterized by a bivalent semantics that distinguishes between the designated values of the logic (the counterparts of the classical value “true”) and the other ones. Furthermore, any such logic can be conservatively extended to a “separable” logic in which this distinction can indeed be expressed by a statement. For separable logics, the authors first devise a cut-free proof formalism based on analytic tableaux that has nodes containing sequences of separating statements. However, these tableaux may be highly branching, which makes them practically unattractive. The method is therefore generalized to a cut-based tableau system that has derivations that are exponentially more succinct and may polynomially simulate the truth-table method.

The paper thus introduces a fresh approach to studying deduction in finite-valued logics. By casting them into the presented framework, different logics may be compared; for example, the tableaux may be used to check whether a rule of one logic is derivable in another. Further work may explore extensions of the presented mechanisms to cover also infinite-valued logics.