Plenary Lecture

Metatheory of Tableau Systems

Professor Tomasz Jarmużek
Departament of Logic
Nicolaus Copernicus University
Toruń, Poland
E-mail: jarmuzek@umk.pl

Abstract: Tableau proofs have a number of advantages in comparison to other proof methods. They can often be conducted automatically and countermodels are often delivered by failed proofs. The advantages are most evident in comparison to standard axiomatic proofs. The chief disadvantage of the tableau method is its intuitiveness, which is extremely problematic in proving soundness and completeness of tableau consequence systems with respect to some semantic consequence relation.
In our talk a perfectly formal account is presented of the question of the tableaux as well as tableau proofs. The approach we propose turns out to be quite successful in dealing with such metalogical problems as soundness and completeness, which will be demonstrated. The account we present extends ideas described in such works as [5], [6], [7]. And we especially extrapolate the tableau method for modal logic, delivered in the work [6] on other kinds of sentential calculi as well as calculi of names.
We begin with a logic, which is to be identified with a particular consequence relation, described semantically. The outcome is a collection of tableau rules that determine together with a concept of tableau proof a tableau consequence relation. Such a collection is called a tableau system. Hence, tableau proofs are regarded a syntactical concept, even if the tableau procedure requires some extensions of the formal language in question. All the tableau concepts we construct are set-theoretical, the graph concept of tableau proof turns out merely didactic presentation of purely formal concepts. And we define generally formal concepts: (a) tableau rule, (b) open, closed and maximal branch, (c) open, closed and complete tableau and (d) branch consequence relation.
By means of such general, formal concepts we are in a position to deliver exact conditions to be satisfied by collections of tableau rules defining tableau systems. In the general metatheory of tableaux we deliver the proofs of metatheorems are included to the effect that equality of the semantical consequence relation and the tableau consequence relation follows from those conditions to be satisfied.
The above mentioned theorem is to be applied to constructions of tableau systems, if the systems are to be sound and complete with respect to a semantical structure. When describing a tableau systems we simply apply general concepts and make sure the rules we formulate meet the formal conditions. If it is the case we immediately obtain a sound and complete calculus.
The theory we deliver covers sentential calculi as well as calculi of names. In our talk we present main metatheoretical concepts, the chief metatheoretical theorem and show some instructive examples of application.

[1] M. D’Agostino, D Gabbay, R Haehnle, J Posegga (Eds), Handbook of Tableau Methods, Kluwer, 1999.
[2] P. Blackburn, M. de Rijke, Y. Venema, Modal Logic, Cambridge, 2002.
[3] Fitting Melvin, First-order logic and automated theorem proving (2nd ed.), Springer-Verlag, 1996.
[4] Priest Graham, An Introduction to Non-Classical Logic, Cambridge University Press, 2001.
[5] Jarmużek Tomasz, Formalizacja metod tablicowych dla logik zdań i logik nazw (Formalization of tableau methods for propositional logics and for logics of names), Wydawnictwo UMK, Toruń, 2013.
[6] Jarmużek Tomasz, ‘Tableau Metatheorem for Modal Logics’, Recent Trends in Philosphical Logic, Trends in Logic, (Eds) Roberto Ciuni, Heinrich Wansing, Caroline Willkomennen, Springer Verlag, 2013, 105–128.
[7] Jarmużek Tomasz, ‘Tableau System for Logic of Categorial Propositions and Decidability’, Bulletin of The Section of Logic, 2008, 37 (3/4), 223–231.
[8] Smullyan Raymond, First Order-Logic, Dover Publications, 1995 (1968).

Brief Biography of the Speaker: TBA

Bulletin Board

Currently:

The Conference Program is online.

The Conference Guide is online.

The paper submission deadline has expired. Please choose a future conference to submit your paper.


Plenary Speakers

WSEAS Main Site

Publication Ethics and Malpractice Statement