# CADE-15 Tutorial: Gentzen-Type Methods in Modal Logics

```
CALL FOR PARTICIPATION

GENTZEN-TYPE METHODS IN MODAL LOGICS

Monday, July, 6, 1998

Arnon Avron
Tel-Aviv University
http://www.math.tau.ac.il/~aa/

The following tutorial will take place on 6/7/98 as one of the
pre-conference workshop and tutorials of the 15th International
Conference on Automated Deduction (Cade98) in Lindau:

GENTZEN-TYPE METHODS IN MODAL LOGICS

Both tableaux methods and resolution methods are closely related
to Gentzen-type proof-theoretical methods (one can argue, in fact,
that they are based on such methods). Researchers in
the domains of Classical logic and Substructural Logics (including
Intuitionistic Logic and Linear Logic) are indeed well acquainted
with the use of sequential calculi. This, unfortunately, is not
the current situation in Modal Logics. Most textbooks in this area
rely on the use of Hilbert-type systems, which are hopelessly
inefficient.  This is the case despite the fact that most (all?) of
the really important Modal Logics have corresponding nice, cut-free
Gentzen-type formulations.

In this tutorial we describe what we believe everyone interested
in Propositional Modal Logic should know concerning the use of
Gentzen-type systems in this field. The logics we treat in detail
are K, K4, D, D4, T, S4, S5, and the provability logics GL and Grz.
The level will mostly be introductory, but some parts will be more

Contents
--------
The following is the list of topics which will be discussed:

1)  The standard Hilbert-type formulations and Kripke-style semantics of
the logics.
2)  The two naturally associated consequence relations and Fitting's
ternary generalization of both.
3)  The standard corresponding Gentzen-type systems.
4)  Finitary and infinitary proofs of various versions of the
cut-elimination theorem.
5)  Applications of cut-elimination (like: completeness, decidability,
interpolation and the modal disjunction property.
6)  The induced tableaux methods.
7)  The source of the difficulty in using resolution for these logics,
and some partial solutions.
8)  The arithmetical interpretations of the provability logics,
and corresponding applications of cut-elimination. The failure for
these logics of cut-elimination in the first-order case.
9)  The failure of cut-elimination for the standard system for S5.
Elimination of analytic-cuts as a substitute.
10) Calculi of hypersequents (finite sets of ordinary sequents).
The cut-free hypersequential formulation of S5.

Organizer
---------
Arnon Avron
Computer Science Department
School of Mathematical Sciences
Tel-Aviv University
Tel-Aviv, Israel

Registration
------------