Skip navigation
The Australian National University

Program outline

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 Gödel 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
Peter Baumgartner
  • Automated propositional theorem proving
  • Automated first-order theorem proving
  • Reasoning with arithmetic constraints by quantifier elimination

Week 2

Deviant Logic
John Slaney
  • Philosophical motivation
  • Routley-Meyer semantics
  • Paraconsistency and the γ rule
  • Deviant theories of arithmetic
Milestones in Descriptive Complexity Theory
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
Verified Verifiers for Verifying Elections
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
Tableaux metatheory for propositional and syllogistic logics
Tomasz Jarmużek
  • TBA
  • TBA
  • TBA

Updated:  19 November 2019 / Responsible Officer:  JavaScript must be enabled to display this email address. / Page Contact:  JavaScript must be enabled to display this email address. / Powered by: Snorkel 1.4