COMP4630/COMP8670 - Overview of Logic and Computation 2019

Introduction

Welcome to COMP4630/COMP8670 for 2019.

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; introduction to untyped and typed lambda calculi.

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.

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. We will also cover the lambda calculus, a model of computation introduced by Alonzo Church. Finally, we shall see how the lambda calculus and logic come together via the Curry-Howard isomorphism to form the basis of most modern functional programming languages, and of most modern interactive proof-assistants.

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.
Develop mathematical proofs in the area of formal logic.

Timetable

Lectures are in the Engineering Lecture Theatre on Monday 1000-1100, Wednesday 1300-1400 and Friday 1100-1200. See the ANU Timetable for COMP4630/COMP8670.

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