Overview of Logic and Computation

This is an introductory post-graduate course given by staff from the Logic and Computation research group.

Untyped Lambda Calculus

These lectures were given in Semester 2 of 2012:

• Lecture 1: Basics
• Lecture 2: Equational Logic
• Lecture 3: Confluence
• Lecture 4: Standardisation
• Lecture 5: Computability

Temporal Logic and Model Checking

These lectures were given in 2008–2011.

• Lecture 1: Modal Logic
• Lecture 2: CTL
• Lecture 3: Explicit State Model Checking
• Lecture 4: BDDs and Symbolic Model Checking
• Lecture 5: Topics in Model Checking (Counter-examples, Bounded Model Checking, Optimisations)
• Lecture 6: LTL Model Checking
• Assessable Exercise (2008–2010): Missionaries and Cannibals

  This exercise requires the use of the SMV tool, which in version 2.4.3 does not compile on some machines because of the code’s use of the reserved function name malloc.  Please apply this patch to fix this problem.

• Assessable Exercise (2011): Colour Rotation Puzzle

Logic Summer School Material

The ANU and NICTA have combined to present two-week long Logic Summer Schools since 2003.  I have taken part in most (all?) of these.

Automated Reasoning: Arithmetic

Slides on arithmetic decision procedures (from February 2009), covering Fourier-Motzkin variable elimination, the Omega Test and Cooper’s method.

Computability and Incompleteness

From December 2009.

• Lecture 1: Computational Models
• Lecture 2: Computability Results
• Lecture 3: Logic and Computability
• Lecture 4: Gödel’s First Incompleteness Theorem
• Lecture 5: Gödel’s Second Incompleteness Theorem

The course referred to the following books:

• Computability and Logic, George Boolos and Richard Jeffrey. ISBN 0-521-38923-2.
• Gödel’s Theorem: An Incomplete Guide to Its Use and Abuse, Torkel Franzén. ISBN 1-56881-238-8.
• Notes on Logic and Set Theory, P. Johnstone. ISBN 0-521-33692-9.
• Introduction to Mathematical Logic, Elliott Mendelson. ISBN 0-412-80830-7.

Other Material

• Lecture given to COMP 2600 (in 2010 and 2011) about the L4.verified project.