# 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

Qing Wang

- Finite model theory
- Inexpressibility proofs
- Descriptive complexity

Michael Norrish

- Computability, recursiveness, Turing machines
- Diagonalisation
- Peano Arithmetic and Goedel 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

Reasoning in Discrete Event SystemsAlban Grastien

- Discrete event systems in artificial intelligence
- Solution methods for DES problems

John Slaney

- Philosophical motivation for substructural logics
- Routley-Meyer semantics
- Paraconsistency and the γ rule
- Deviant theories of arithmetic

Sophie Pinchinat

- From Dynamics to Knowledge (Epistemic Temporal Logics)
- From Knowledge to Dynamics (Dynamic Epistemic Logic)
- Strategic Reasoning

Christoph Benzmüller and

Bruno Woltzenlogel Paleo

- Overview and Introduction to Higher-Order Logics (HOL)
- Higher-Order Modal Logics (HOML) and their embedding into HOL
- Application: Gödel’s Ontological Argument and its variants
- Applications of HOML for the Semantic Web and Ontology Reasoning

James Brotherston

- Boolean bunched logic and its semantics
- Proof theory for Boolean bunched logic
- Undecidability of Boolean bunched logic
- Definability in Boolean bunched logic
- From Boolean bunched logic to separation logic