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.
- Lecture given to COMP 2600 (in 2010 and 2011) about the L4.verified project.