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

Deep Inference
Alwen 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
Deviant Logic
John Slaney
  • Philosophical motivation
  • Routley-Meyer semantics
  • Paraconsistency and the γ rule
  • Deviant theories of arithmetic
Proof Complexity
Olaf Beyersdorff
  • propositional proof systems
  • lower bound techniques
  • hard formulas
  • automatisability
  • relations to SAT/QBF solving
  • proof complexity of QBF and modal logic
Modal Reasoning through Resolution
Cláudia Nalon
  • Introduction to propositional modal logic
  • Resolution for classical propositional logic
  • Non-clausal resolution for modal logics
  • Clausal resolution for modal logics

Updated:  1 December 2017 / 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