FDD3029 Epistemic Logic 6.0 credits

One two-hour lecture per week for 7 weeks. Topical homework every week (graded in batches of 2 weeks), a take-home final exam, and a practical project.

We introduce epistemic logic, a modal logic that we use to represent and reason about knowledge formally. We will study its theoretical foundations, including possible-worlds models and axiomatisations whose soundness and completeness we will prove, and explore applications in domains ranging from mathematical puzzles to formal games, distributed systems and computer security. The goal is to cover most of chapters 1-4 and parts of chapter 5 of Reasoning about Knowledge, as well as some more recent applications that postdate the book.

The course is broadly divided into two halves, with 4 weeks covering the broadly-applicable theoretical basics of epistemic logic, and another 3 weeks exploring its applications to a variety of problems in computer science including distributed systems and security.

The student will be able to 

• articulate the challenges of formally representing knowledge, and explain how these are addressed using epistemic logic and the possible-worlds model of knowledge
• interpret epistemic formulae in the possible-worlds model
• prove and disprove tautologies using both semantic approaches and formal deduction on formulae
• describe various models and axiomatisations for modal logics, and prove an axiom system sound and complete
• use epistemic logic to formalise and reason about problems involving knowledge in areas such as program analysis, distributed systems and protocols and game theory
• understand and implement tools for automated reasoning with epistemic logic

None

Familiarity with propositional logic and mathematical proofs, as well as programming skills in a general-purpose language.

Computer with working programming environment

Reasoning about Knowledge (Fagin, Halpern, Moses and Vardi), MIT Press 2004

If the course is discontinued, students may request to be examined during the following two academic years.

• EXA1 - Examination, 6.0 credits, grading scale: P, F

Based on recommendation from KTH’s coordinator for disabilities, the examiner will decide how to adapt an examination for students with documented disability.

The examiner may apply another examination format when re-examining individual students.

The course will be examined based on 3 graded homeworks, a final take-home exam, and a programming project in which the student will implement a model checker for epistemic logic.

Musard Balliu

• All members of a group are responsible for the group's work.
• In any assessment, every student shall honestly disclose any help received and sources used.
• In an oral assessment, every student shall be able to present and answer questions about the entire assignment and solution.