Week 1

Fundamentals of Metalogic
John Slaney

• Metatheory of classical first-order logic, including completeness theorem
• Basics of proof theory
• The Joy of Sets

Computability and Incompleteness
Michael Norrish

• Computability, recursiveness, Turing machines
• Diagonalisation
• Peano Arithmetic and Goedel numbering
• Undecidability of first-order logic
• Incompleteness of Peano Arithmetic

Introduction to Modal and Temporal Logic
Rajeev Gore

• Kripke models, Hilbert calculi, Frame correspondences
• Tableaux-based decisions procedures
• Propositional linear temporal logic

Overview of Automated Reasoning
Presenter TBA

• Automated propositional theorem proving
• Automated first-order theorem proving
• Reasoning with arithmetic constraints by quantifier elimination

Week 2

5 courses TBA