The goal of the Autumn School on Modal Logic is to prepare PhD students and other researchers for participation in the sixth workshop Methods for Modalities (M4M-6) which takes place November 12-14 2009 in Copenhagen. The workshop Methods for Modalities aims to bring together researchers interested in developing proof tools and decision methods based on modal logics. Here the term "modal logics" is conceived broadly, including description logic, guarded fragments, conditional logic, temporal and hybrid logic, etc. The first M4M workshop took place in Amsterdam in 1999. Since then, M4M workshops have taken place in 2001 (Amsterdam), 2003 (Nancy), 2005 (Berlin), and 2007 (Paris). See Methods for Modalities for more information on the workshop series, in particular, see why modal logic is important for computer science. A goal of having M4M in Denmark is to strengthen Danish research in reasoning methods for modal logics, which is a growing area of foundational and increasingly computational importance.
The Autumn School on Modal Logic is open to anyone interested. The intended participants will have a general background in theoretical computer science, but wish to obtain more concrete knowledge on modal logic and its computational aspects. Besides a working knowledge of English, prerequisites are a basic knowledge of logic and mathematics that is usually covered in undergraduate classes on discrete mathematics.
by Carlos Areces and Patrick Blackburn, INRIA, Nancy
In this course, we will present some classical results of modal logic taking a computational approach. Our definition of what a 'modal' language is will be particularly broad including, in addition to standard modal languages, propositional logic, description logics, hybrid logics, first-order logic and higher-order logics. Our goal is to show that the modal approach provides a very cohesive perspective. [Material]
by Valentin Goranko, Technical University of Denmark
I will discuss formal specification and verification of properties (safety, eventualities, fairness) of transition systems and how temporal logics can be used for that purpose. I will introduce briefly the linear and branching time temporal logics (LTL and CTL). [Material1] [Material2]
by Carsten Schürmann, IT University of Copenhagen
In this course, we reconsider the foundations of intuitionistic modal logic, following Martin-Löf's methodology of distinguishing judgments from propositions. We give constructive meaning explanations for necessity and possibility, and if time permits, we will discuss modalities that correspond to categorical judgments. The goal of this course is to give students an introduction to modal logic the proof theory way as opposed to the usual model theoretic way. [Material]
by Renate Schmidt, University of Manchester
Many modal and description logics can be seen as fragments of first-order logic. We explore the possibilities of using techniques and tools from first-order logic and resolution for deciding dynamic modal logics. Dynamic modal logics are extensions of multi-modal K with relational operators which are closely related to description logics. Time permitting we will mention other applications such as automatic model generation and automated correspondence theory. [Material 1] [Material 2]
by Patrick Blackburn, INRIA, Nancy
In this talk, after introducing the basics of hybrid logic, I will discuss hybrid deduction from both tableau-based and axiomatic perspectives. I will draw attention to what is common to both, and explain the pervasive role of Henkin models in hybrid completeness theory.
A diploma will be available to all PhD students succesfully completing the course. Succesful completion requires presence and active participation. The course yields 2.5 ECTS (European Credit Transfer System).
The school takes place at the IT University of Copenhagen (close to the venue of M4M-6, which is the IDA Conference Center). Both venues are within walking distance from the city center of Copenhagen. The autumn school takes place in the room of the IT University called the "Scrollbar".
The IT University of Copenhagen is located 3 km from Copenhagen Central Station. To get directions on how to get there on foot from the central station, click here. Alternatively, one can take an S-train from the central station to Nørreport Station, and then the Metro from Nørreport Station to the station "DR Byen/Universitetet".
Further travelling information and information concerning accommodation can be found at the M4M-6 home page.
Registration is via the M4M-6 registration page. The FIRST Research School covers the registration fee for all PhD students affiliated with FIRST (but registration is required in any case). Registration deadline: November 5th.
Thomas Bolander, Technical University of Denmark, tb@imm.dtu.dk
Torben Braüner, Roskilde University, torben@ruc.dk
Carsten Schürmann, IT University of Copenhagen, carsten@itu.dk
Torben Braüner is main organizer of the school and can be contacted for more information. The Autumn School on Modal Logic is supported by the FIRST Research School and the project Hybrid Logic, Computation, and Reasoning Methods (HYLOCORE).