nicta logo

NICTA Advanced Course

Theorem Proving - Principles, Techniques, Applications

Intro Session times Links  

This is an advanced NICTA course aimed at fourth year and postgraduate students. It is provided at UNSW, ANU, and University of Melbourne across a video link from the NICTA Formal Methods program based at UNSW/Sydney.

There is no formal enrollment at ANU, UNSW, or Melbourne necessary. Please send an email to Gerwin Klein <> if you would like to be included in the lecture mailing list. The course is free, there will be no assignments, but also no credits.

Presenter: Gerwin Klein (NICTA/Formal Methods)

This course is about mechanical proof assistants, how they work, and what they can be used for. It presents specification and proof techniques used in industrial grade theorem provers, teaches the theoretical backround to the techniques involved, and shows how to use a theorem prover to conduct formal proofs in practice. The course is intended to bring fourth year and postgraduate students into contact with current research topics in the field of theorem proving and automated deduction and to teach them the necessary skills to successfully use industrial grade verification environments in modelling and verification.

Topics include higher order logic, natural deduction, lambda calculus, term rewriting, data types and recursive functions, induction principles, calculational reasoning, mathematical proofs, and proofs about programs.


Session times:



More information and lecture slides will be made available on this page during the course.


Further Reading:


  Gerwin Klein Last modified: Mon Sep 20 14:07:12 EST 2004