15-816 Modal Logic

Spring 2010

Frank Pfenning and André Platzer

TuTh 1:30-2:50

GHC 4102

12 units

Preliminary Information Below

Modal logic is the study of the laws of inference for judgments such as "it is necessary that", "it is possible that", "K knows that", "K affirms that", etc. Its roots lie in philosophy and linguistics, but it has a suprisingly rich variety of applications in computer science. This course provides a thorough introduction to both classical and intuitionistic modal logic, with an emphasis on applications in computer science. This class will study the proof theory and meta theory of modal logics, and present the foundations for practical proof procedures.

Specific topics include: intuitionistic logic, justification of logical laws, judgmental S4 and staged computation, classical modal logics, axiom systems, Kripke semantics, correspondence theory, intuitionistic S5 and distributed computation, sequent calculi, cut and identity properties, tableaux systems, completeness of classical modal logics, canonical models and filtration, decidability, focusing, substructural logics as modal logics, constructive resource semantics, description logics, first-order modal logics, dynamic logic, modal type theories, logics of affirmation and knowledge.

Students from mathematics and philosophy, as well as enterprising undergraduate with a basic foundation in logic are invited.

Prerequisites: For undergraduates, 15-317 Constructive Logic or 15-312 Foundations of Programming Languages. No prerequisites for graduate students.

What's New?

(9/9) If you want access to the coursecast video captures of this course, please send an email to the course instructors.
(5/11) Final project reports have been posted, accessible from *.cmu.edu only.
(3/30) Notes on Lecture 18 on Model Checking posted

projects

(2/23) Notes on Lecture 11 on Soundness of Modal Tableaux and Assignment 5 has been posted.

07-cor.pdf

(2/16) Notes for Lecture 9 on Combinatory Modal Logic and Assignment 4 have been posted.
(2/12) Notes for Lecture 8 on Sequent Calculus have been posted.
(2/8) Correction posted for Exercise 7.3. The formula I meant is: [](a ∧ []a → b) ∨ [](b ∧ []b → a)
(2/4) No class, special seminar Vladimir Voevodsky at 1pm instead.
(2/2) Assignment 3 has been posted. Its due date is Tue Feb 9.
(2/2) Notes for Lecture 7 have been posted.
(1/26) The proposed substitution principle in Exercise 4.2 was wronger than I had intended.
I meant to say: If Δ ; Γ |- A poss and Δ ; x:A |- C true then Δ ; Γ |- C true.
(1/26) Notes for Lecture 5 and 6 have been posted.
(1/24) Assignment 2 has been posted. Its due date has been pushed back to Tue Feb 2.
(1/15) Assignment 1 has been posted, together with a LaTeX example, which might be helpful for those who wish to typeset their answers.
(1/15/2010) Notes for Lecture 1 and Lecture 2 have been posted.
(11/11/2009) Preliminary website created.

Class Material

Schedule	Lecture schedule, readings, code
Assignments	Details of assignments, due dates, policies
Projects	Project information
Handouts	Collected handouts
Resources	Other course resources

Course Information

Lectures	TuTh 1:30-2:50, GHC 4102
Office Hours	TBA
Notes	There is no textbook, but notes on Modal Logic and papers will be handed out.
Credit	12 units
Grading	50% Homework, 15% Midterm, 35% Project.
Homework	Weekly homework for the first n weeks of the course goes out Thursday and is due the following Thursday. 500 pts.
Exams	Midterm, in class, Thu Mar 4, 1:30-2:50. Closed book, with one two-sided sheet of notes permitted. 150 pts.
Project	Due Fri May 7. Projects with groups of 2 or 3 students are encouraged; must have a term paper and possibly an implementation. Some suggestions will be offered, but student creatitivity in encouraged. 350 pts.
Mailing List	modlog-course@cs Subscribe at https://mailman.srv.cs.cmu.edu/mailman/listinfo/modlog-course
Home	http://www.cs.cmu.edu/~fp/courses/15816-s10/

fp@cs, aplatzer@cs
Frank Pfenning, André Platzer