The origin of dual tableaux goes back to the paper [RAS60] of Rasiowa and Sikorski, where a cut-free deduction system for the classical first-order logic has been presented. Systems in the Rasiowa-Sikorski style are top-down validity checkers and they are dual to the well known tableau systems. The common language of most of relational dual tableaux is the logic of binary relations which was introduced in [ORL88] as a logical counterpart to the class of representable relation algebras given by Tarski in [TAR41]. The relational methodology enables us to represent within a uniform formalism the three basic components of formal systems: syntax, semantics, and deduction apparatus. Hence, the relational approach can be seen as a general framework for representing, investigating, implementing, and comparing theories with incompatible languages and/or semantics. Relational dual tableaux are powerful tools which perform not only verification of validity (i.e., verification of truth of the statements in all the models of a theory) but often they can also be used for proving entailment (i.e., verification that truth of a finite number of statements implies truth of some other statement), model checking (i.e., verification of truth of a statement in a particular fixed model), and finite satisfaction (i.e., verification that a statement is satisfied by some fixed objects of a finite model). This presentation is an introductory overview on specific methodological principles of constructing relational dual tableaux and their applications to nonclassical logics. In particular, we will present relational dual tableaux for standard non-classical logics (modal, intuitionistic, relevant, many-valued) and for various applied theories of computational logic (fuzzy-set-based reasoning, qualitative reasoning, reasoning about programs, among others). Furthermore, we will discuss decision procedures in dual tableaux style. By way of example, we will show how to modify the classical dual tableau systems to obtain decision procedures for some modal and intuitionistic logics.
Joanna Golin`ska-Pilarek