=Paper=
{{Paper
|id=None
|storemode=property
|title=Relational Dual Tableaux: Foundations and Applications
|pdfUrl=https://ceur-ws.org/Vol-1068/paper-i01.pdf
|volume=Vol-1068
|dblpUrl=https://dblp.org/rec/conf/cilc/Golinska-Pilarek13
}}
==Relational Dual Tableaux: Foundations and Applications==
<pdf width="1500px">https://ceur-ws.org/Vol-1068/paper-i01.pdf</pdf>
<pre>
    Relational Dual Tableaux: Foundations and
                   Applications

                             Joanna Goliǹska-Pilarek

                   Institute of Philosophy, University of Warsaw



    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 for-
malism 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 theo-
ries 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., verifi-
cation 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 prin-
ciples of constructing relational dual tableaux and their applications to non-
classical logics. In particular, we will present relational dual tableaux for stan-
dard non-classical logics (modal, intuitionistic, relevant, many-valued) and for
various applied theories of computational logic (fuzzy-set-based reasoning, qual-
itative 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.

   References
    [GHM13] J. Goliǹska-Pilarek, T. Huuskonen, E. Munoz-Velasco, Relational
dual tableau decision procedures and their applications to modal and intuitionistic
logics, forthcoming in Annals of Pure and Applied Logics, doi: 10.1016/j.apal.2013.06.003
    [ORG11] E. Orlowska, J. Goliǹska-Pilarek, Dual Tableaux: Foundations, Method-
ology, Case Studies, Springer, 2011.
16                                                         Joanna Goliǹska-Pilarek


     [ORL88] E. Orlowska, Relational interpretation of modal logics, in: H. An-
 dreka, D. Monk, I. Nemeti (eds.), Algebraic Logic, Colloquia Mathematica So-
 cietatis Janos Bolyai 54, North Holland, Amsterdam, 1988, 443-471.
     [RAS60] H. Rasiowa, R. Sikorski, On Gentzen theorem, Fundamenta Mathe-
 maticae 48 (1960), 57-69.
     [TAR41] A. Tarski, On the calculus of relations, Journal of Symbolic Logic 6
 (1941), 73- 89.

</pre>