Relational Dual Tableaux: Foundations and Applications JoannaGoliÇıska-Pilarek Institute of Philosophy University of Warsaw Relational Dual Tableaux: Foundations and Applications 2B007297B519F77FCB58146771F2B435 10.1016/j.apal.2013.06.003 GROBID - A machine learning software for extracting information from scholarly documents

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.

Relational dual tableau decision procedures and their applications to modal and intuitionistic logics JGoliÇıska-Pilarek THuuskonen EMunoz-Velasco 10.1016/j.apal.2013.06.003 forthcoming in Annals of Pure and Applied Logics EOr Lowska JGoliÇıska-Pilarek Dual Tableaux: Foundations, Methodology, Case Studies Springer 2011 Relational interpretation of modal logics EOr Lowska Algebraic Logic Colloquia Mathematica Societatis Janos Bolyai HAndreka DMonk INemeti
North Holland, Amsterdam
 1988 54 On Gentzen theorem HRasiowa RSikorski Fundamenta Mathematicae 48 1960 On the calculus of relations ATarski Journal of Symbolic Logic 6 1941