CECS Home | ANU Home | Search ANU
The Australian National University
ANU College of Engineering and Computer Science
Department of Computer Science
COMP4630/COMP6463
Introduction
Schedule and Notes
Labs and Tutorials
Assignments
Assessment Scheme
Marks and Lab Registration
Reading Material
Forums
People
CECS Links
DCS Home
CECS Home
ANU Home
Printer Friendly Version of this Document

UniSAFE

COMP4630/COMP6463 - Overview of Logic and Computation

Introduction

Welcome to COMP4630/COMP6463 for 2009.

Prerequisites

COMP4630: 24 units of 3000-level COMP courses including COMP3610.

Syllabus

This course covers: essentials of first order logic, up to and including completeness proofs; introductions to proof theory and model theory; elements of modal and temporal logic; introduction to automated reasoning.

Rationale

(Mathematical) logic has been called the 'Calculus of Computer Science' and it is the main theoretical tool to describe computation. Implemented systems for logical reasoning are routinely used by industry today, e.g., for software and hardware verification. The rationale behind this course is that understanding the concepts of logic and computation is a valuable preparation for further studies in theoretical computer science and its application in the real world.

Contents

The course starts with foundational issues of mathematical logic, cast in stone for a long time, before computers were around. It then turns to questions of bringing logic to computer. It covers important logics that can successfully be implemented on computer: propositional logic, first-order logic and certain temporal logics. The latter is used for verification of dynamic properties of reactive systems (an operating system is an example for such a system). It is a special case of a so-called modal logic, a family of logics that are, in their full generality, much richer than the above mentioned logics. Modal logics are covered as well.

Outcomes

On satisfying the requirements of this course, students will have the knowledge and skills to:

  • Define several formal logical languages, their syntax and semantics.
  • Explain inference mechanisms and their theoretical properties.
  • Demonstrate how these languages and inference mechanisms can be applied to model and solve problems.
  • Experiment with computer programs for automated reasoning.
  • Develop mathematical proofs in the area of formal logic.

Timetable

Lectures and Tutorials are on Monday, Tuesday and Wednesday. See the ANU Timetable for COMP4630/COMP6463.

See also the Schedule for a breakdown of course contents into lectures.

The room is N329 "Aquarium".

The course proper starts in week 2.

You might also find the Principal Academic Dates for 2008 useful. They include the start and end dates for each teaching period.

Course Information

Study@ANU entries show details of the course including pre-requisites.

Lectures and Tutes

Suggested reading for lectures can be found on the Schedule and Notes page.

Additional Information

Yes, the course does take place.

Last updated Mon Feb 16 15:12:33 EST 2009 by u1447109
Please direct all enquiries to: consultant@cs.anu.edu.au
Page authorised by: Head of Department, DCS
The Australian National University — CRICOS Provider Number 00120C