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
Finite model theory
Qing Wang
  • Finite model theory
  • Inexpressibility proofs
  • Descriptive complexity
Computability and Incompleteness
Michael Norrish
  • Computability, recursiveness, Turing machines
  • Diagonalisation
  • Peano Arithmetic and Goedel 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

Reasoning in Discrete Event Systems
Alban Grastien
  • Discrete event systems in artificial intelligence
  • Solution methods for DES problems
Deviant Logic
John Slaney
  • Philosophical motivation for substructural logics
  • Routley-Meyer semantics
  • Paraconsistency and the γ rule
  • Deviant theories of arithmetic
Logics in Multi-agent Systems
Sophie Pinchinat
  • From Dynamics to Knowledge (Epistemic Temporal Logics)
  • From Knowledge to Dynamics (Dynamic Epistemic Logic)
  • Strategic Reasoning
Higher order Modal Logic
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
Bunched Logic to Separation Logic
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

Updated:  5 December 2015 / 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