(unknown)

 cas-+VuHOhYSxa2v/2WfcVMNQPhqMcnVdK/bs0AfqQuZ5sE@xxxxxxxxxxxxxxxx
Received: from cas by sarpedon with local (Exim 3.35 #1)
        id 1CKuf2-0000YW-00; Fri, 22 Oct 2004 08:20:32 +0000
From:  <cas@dialup>
To: Frogs <Frogs-+VuHOhYSxa2v/2WfcVMNQPhqMcnVdK/bs0AfqQuZ5sE@xxxxxxxxxxxxxxxx>
cc: Valeria.dePaiva-JIACEBSeTWI@xxxxxxxxxxxxxxxx, 
Subject: Proof theory of modal logic
X-Mailer: Jade 4.0-alpha
Message-Id: <E1CKuf2-0000YW-00@sarpedon>
Date: Fri, 22 Oct 2004 08:20:32 +0000
X-diagnostic: ferry_transport


Hello,

Phiniki Stouppa has submitted her MSc thesis to her examiners, and will
be defending her thesis on 27th October (ie. next Wednesday).  Her thesis
is available for download from:
  http://www.linearity.org/cas/supervision/
and is titled:
  The design of Modal Proof Theories: the case of S5
(52 pages, PDF file)

What she has done in her thesis is threefold:
  (i) She has given a selective survey of proof theories of modal logic
  that provide some sort of Hauptsatz for S5. narrowing in on those that
  are "conceptually pure", ie. which do not make use of devices that go
  beyond the concepts of propositional logic and modality (for example,
  this excludes various labelled calculi).
  (ii) She provides a much needed attempt to give criteria that can help
  us identify what approaches give good proof theories; this builds on the
  similar attempt provided in Heinrich Wansing's Habilitation thesis.
  (iii) She presents a system for S5 in the calculus of structures, which
  she shows to satisfy cut-admissibility.  This result was described in
  the Advances in Modal Logic paper; the thesis provides the first complete
  proof of this.  This calculus, naturally, has excellent properties.

The thesis is very readable, and I urge anyone interested in the connection
between deep inference and modality to take a look at it.  And, of course,
to wish her luck on Wednesday.

Additionally, Phiniki will start her course of study towards her PhD
next month in Berne, working in the same department as Kai.

Charles