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.
展开▼
