Modal Logic and Proof Theory
Faculteit  Science and Engineering 
Jaar  2022/23 
Vakcode  WMCS02705 
Vaknaam  Modal Logic and Proof Theory 
Niveau(s)  master 
Voertaal  Engels 
Periode  semester I b 
ECTS  5 
Rooster  rooster.rug.nl 
Uitgebreide vaknaam  Modal Logic and Proof Theory  
Leerdoelen  At the end of the course, the student is able to: 1) Present sequent calculi for classical and intuitionistic logic and for selected modal and substructural logics, and explain their meaning as formal proof systems. 2) Formulate the cutelimination argument and subformula property, and use a cutfree sequent calculus to investigate and prove selected properties of a logic. 3) Apply modal logic to specify and reason about relational and neghbourhood structures. 4) Carry out mathematical proofs and constructions to establish properties such as completeness and the finite model property of some basic modal logics. 

Omschrijving  The course provides an introduction to modal logics and substructural logics, their applications in CS, and their proof theoretic and computational properties. Modal logics are a family of logics that extend classical logic through the addition of modal operators. They are widely used as specification languages in formal verification due to the good balance between their expressive power and computational complexity. Substructural logics omit some of the structural properties of classical logic (properties we might take for granted, like commutativity or weakening), so acquiring a resource awareness that has been utilised in areas such as verification and computational linguistics. The first part of the course is an introduction to proof theory. The starting point is the sequent calculus for classical propositional logic and Gentzen's landmark cutelimination theorem whose consequence is the subformula property. Applications of the subformula property follow and include arguments for consistency, decidability, and complexity. These ideas and results are then extended to the setting of modal and substructural logics. We will also take the opportunity to discuss some interpolation and Glivenko theorems. The second part of the course will introduce normal and nonnormal modal logics as specification languages for models that formalize, e.g., program behavior and strategic interaction in games. We will examine their expressive power and basic model theory. Basic concepts that will be covered include: Kripke semantics, neighbourhood semantics, morphisms, bisimulations, definability, filtrations, Hilbert systems, and completeness via canonical models. 

Uren per week  
Onderwijsvorm  Hoorcollege (LC), Opdracht (ASM), Werkcollege (T)  
Toetsvorm 
Opdracht (AST)
(The final grade is based on 4 individual assignments: two for proof theory, two for modal logic, each counting for 25%. Each of the four assignments must receive a grade of 5.0 or higher. If an assignment does not meet the 5.0 mark, a retake assignment must be completed. A retake assignment can receive a maximum grade of 7.0.) 

Vaksoort  master  
Coördinator  Prof. Dr. H.H. Hansen  
Docent(en)  Prof. Dr. H.H. Hansen , D.R.S. Ramanayake, PhD.  
Verplichte literatuur 


Entreevoorwaarden  The course assumes students are familiar with Propositional Logic, FirstOrder Logic, and basic discrete mathematics (sets, functions, relations). It is also assumed that students are able to carry out mathematical proofs, including induction proofs. From the BSc Computing Science: Introduction to Logic, Discrete Structures, and Languages and Machines.  
Opmerkingen  This course has limited enrollment:  CS students can always enter the course, regardless of whether the course is mandatory for them or not.  A maximum of only 20 places per course is available for nonCS students. These places are filled on a firstcomefirstserved basis, with priority given to students with a strong CSrelated background (e.g., CS exchange students, AI students, etc.). These students need to meet the course prerequisite requirements as mentioned on Ocasys. Six weeks before the course starts, the 20 students that can join are selected and added to the course. If you enroll after this date, you will be placed on the waiting list. For more info about the enrollment procedure, see https://student.portal.rug.nl/infonet/studenten/fse/programmes/msccs/general/vakintekeningprocedure#cap 

Opgenomen in 
