Overview of Logic and Computation COMP6463

Course overview

Course description

This broad 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. There will be 2 lectures per week and weekly tutorial-style meetings. 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

• Introduction to Logic (First-Order Logic, Calculi, Soundness and Completeness)
• Automated Reasoning in First-Order Logic
• Automating Propositional Logic (SAT solving)
• Modal Logic
• Temporal Logic (LTL and CTL, model checking)

Technical skills

Basic knowledge in algebra

Workload

Partly 2 hours of lecture and a one-hour tutorial, partly 3 hours of lecture, for 12 weeks. Students can expect to undertake 3 hours of study per week outside class time.