Program outline
Week 1
Fundamentals of MetalogicJohn Slaney
- Metatheory of classical first-order logic, including completeness theorem
- Basics of proof theory
- The Joy of Sets
Michael Norrish
- Computability, recursiveness, Turing machines
- Diagonalisation
- Peano Arithmetic and Gödel numbering
- Undecidability of first-order logic
- Incompleteness of Peano Arithmetic
Rajeev Gore
- Kripke models, Hilbert calculi, Frame correspondences
- Tableaux-based decisions procedures
- Propositional linear temporal logic
Peter Baumgartner
- Automated propositional theorem proving
- Automated first-order theorem proving
- Reasoning with arithmetic constraints by quantifier elimination
Week 2
Deviant LogicJohn Slaney
- Philosophical motivation
- Routley-Meyer semantics
- Paraconsistency and the γ rule
- Deviant theories of arithmetic
Sasha Rubin
- Lec 1: Games: Model checking first-order logic using a game-based approach
- Lec 2: Kozen: Model checking fixpoint logic using parity games
- Lec 3: Fagin: Capturing NP
- Lec 4: Buchi-Elgot-Trakhtenbrot: Capturing regular languages
- Lec 5: Immerman-Vardi: Capturing P on ordered structures
Thomas Haines
- Lecture 1: Groups and Commitments
- Lecture 2: Encryption Schemes
- Lecture 3: Sigma Protocols
- Lecture 4: Electronic Voting Schemes
- Lecture 5: From Sigma Protocols to Mix nets
Tomasz Jarmużek
- TBA
- TBA
- TBA
