Logic and Computation Group: Courses

The following are short descriptions of courses currently on offer. This page should be read in conjunction with those of the College of Engineering and Computer Science concerning the MICT and the PhD degrees.

Advanced undergraduates may in most cases enrol in these courses by permission of the presenters and of the appropriate Head of Department. At some stage (maybe 2008) such courses will be made available remotely to students at the University of New South Wales, the University of Melbourne and elsewhere.

Overview of Logic and Automated Reasoning
MICT course, semester 1, 2007.
Presenters: Rajeev Goré, Jinbo Huang, John Slaney

Review of first order logic: logic as a knowledge representation medium. Basics of metalogic up to and including completeness of first order logic. Introduction to modal and temporal logics. Elements of automated reasoning: SAT solving; resolution and similar techniques; knowledge compilation.

Automated Reasoning
MICT advanced course, semester 1, 2007.
Presenters: Peter Baumgartner, Jia Meng, Michael Norrish

This course goes into some detail concerning both first order and higher order reasoning. We examine the standard algorithms for mechanical deduction and some alternatives to them, concentrating particularly on "instance-based" methods. We also examine tactic-based interactive theorem proving. This is a "hands-on" course: students are expected to study and learn to use contemporary reasoning software including the first order theorem prover Darwin and the interactive systems HOL and Isabelle.

Non-classical Logic
MICT advanced course, semester 2, 2007.
Presenters: John Slaney, Alwen Tiu

Examination of a range of non-classical logics including modal and substructural logics. We treat the formal systems from the standpoints of proof theory and model theory, and consider some of their actual and potential applications. The format of the course is rather informal, with students expected to present material in a seminar style and to discuss what is presented.