[Prev][Next][Index][Thread]

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


			CALL FOR PARTICIPATION

			 CADE-15 TUTORIAL ON

		 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 
advance.


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
------------
Please use the CADE registration form

http://aida.intellektik.informatik.tu-darmstadt.de/~cade-15/RegoForm.html


Further information
-------------------
CADE-15 Web Site -- http://www.tu-darmstadt.de/cade-15/
TUTORIAL Web Site -- http://www.math.tau.ac.il/~aa/cade/cade.html