Overview of Logic and Computation COMP4630

Course overview

Course description

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. Students will have the opportunity to read and present material going beyond that in the lectures.

Course content

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.

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.

Ideas

This course will carry the main responsibility for:

• Automatic and interactive theorem proving,
• Formal methods for software engineering,
• Representation of knowledge.

Topics

The following topics will be covered:

• Representation of knowledge
• Automatic theorem proving
• Heuristic search
• Models of concurrency

Workload

Twenty-six one-hour lectures, ten one-hour tutorials