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
Deep InferenceAlwen Tiu
- Introduction to deep inference
- SKS: deep inference for classical logic
- External cut-elimination for SKS
- Internal cut elimination for SKS
- System BV: a non-commutative logic
- The need for deep inference
- Application: modelling process calculus in BV
John Slaney
- Philosophical motivation
- Routley-Meyer semantics
- Paraconsistency and the γ rule
- Deviant theories of arithmetic
Olaf Beyersdorff
- propositional proof systems
- lower bound techniques
- hard formulas
- automatisability
- relations to SAT/QBF solving
- proof complexity of QBF and modal logic
Cláudia Nalon
- Introduction to propositional modal logic
- Resolution for classical propositional logic
- Non-clausal resolution for modal logics
- Clausal resolution for modal logics
