Skip to navigation | Skip to main content | Skip to footer

COMP20142: Logic in Computer Science (2008-2009)

This is an archived syllabus from 2008-2009

Logic in Computer Science
Level: 2
Credit rating: 10
Pre-requisites: COMP10020 or equivalent (e.g. COMP10021 or MATH10111 and MATH10131 and MATH10212 and MATH10232)
Co-requisites: No Co-requisites
Duration: 11 weeks in second semester
Lectures: 22 in total, 2 per week, including some feedback sessions on exercises
Lecturers: Andrei Voronkov
Course lecturer: Andrei Voronkov

Additional staff: view all staff
Sem 2 w19-26,30-33 Lecture 1.4 Thu 10:00 - 11:00 -
Sem 2 w19-26,30-33 Lecture 1.5 Fri 15:00 - 16:00 -
Assessment Breakdown
Exam: 80%
Coursework: 0%
Lab: 0%


This course intends to build an understanding of fundamentals of (mathematical) logic as well as some of the applications of logic in modern computer science, including hardware verification, finite domain constraint satisfaction, and databases.

Learning Outcomes

A student completing this course unit should:
Have a knowledge about basic reasoning (or satisfiability-checking) algorithms for propositional logic (A).
To understand BDDS (binary decision diagrams) as a data structure for compact representation of propositional formulas (A).
Have a knowledge about applications of propositional logic (such as finite domain constraint satisfaction and planning) and be able to apply it for solving hard combinatorial problems (B and C).
Have a knowledge of simple temporal logics (A).
Be able to specify properties of simple finite-state systems in temporal logics (B).
Be able to use first-order logic for knowledge representation (A).
To understand relations between logic and database query languages (A).

Assessment of Learning outcomes

Learning outcomes (1), (2) and (6) are assesed both by examination and exercises. Learning outcomes (3), (4), (5) and (7) are assessed by examination.

Contribution to Programme Learning Outcomes

A1, A2, A5, B1, C5 and C6.


Lectures 1-6. Propositional logic

Syntax and semantics. Validity and satisfiability. Satisfiability checking. Splitting and tableau-based algorithms for satisfiability checking. Binary decision diagrams. Propositional logic and finite-domain constraint satisfaction.

Lectures 7-12. Temporal logic

Syntax and semantics. Kripke structures. Specification of concurrent systems in temporal logic. Automatic verification of concurrent systems by model checking.

Lectures 13-18. First-order logic

Syntax and semantics. Reasoning in first-order logic.

Lectures 19-24. Logic in databases

Logic and database query languages. Datalog and relational algebra. Logic and recursion.

Reading List

There is not one particular book that covers the course material entirely. For this reason there will be a set of notes.