CS2142 Logic in Computer Science (2006)


Results and solutions to Assignment 4 are available now. If you have questions related to the assignments/marks please see Mohammed Jaber room 2.108.

Revision Session: May 26 Room 1.3, 15:00.

General information

The aim this course is to give introduction to logic for computer scientists and show applicability of logic in a number of important areas of computer science.

The content of the course will be similar to the previous year course. I will give a slightly more advanced material but there will be no radical changes.

This Web page will contain all up-to-date material on this course.


The assessment of this course consists of assessed exercises during the course (20%) and an examination (80%). Each assessed exercise has an associated deadline, see the course schedule. The solutions can be given to me at a lecture or to Mohammed Jaber (2.116) before the deadline.


There will be handouts, generally distributed at each lecture. There will be two kind of handouts: slides and lecture notes. They will also be put on the Web pages of this course. If you did not attend the lecture, the only way to get handouts is to download them from the Web pages.

CS2142 Schedule (2006)

CS2142 Schedule (2006)

All material referred to from this page (such as slides or reading material) is initially taken from the last year course and will be updated during the course. In the reading material, the date of writing can be seen on the bottom of each page.

All Lectures will be given in Room 1.3.

  date topic chapters slides assignment deadline results solutions
1 Feb 2 Introduction. Propositional Logic. 2, 3 slides        
2 Feb 3 Propositional Logic. Satisfiability. 3 slides        
3 Feb 9 Satisfiability Checking. 4 slides        
4 Feb 10 Polarity. CNF 4, 5 slides pdf file Mar 3 results solution
5 Feb 16 CNF and clausal form. Unit propagation 5 slides        
6 Feb 17 Optimised Definitional Transformation. DLL. 5 slides        
7 Feb 23 SAT and Randomisation. 8 slides        
8 Feb 24 Semantic Tableaux. 9 slides        
9 Mar 2 BDDs and OBDDs 10 slides        
10 Mar 3 OBDD Algorithms. 10 slides pdf file Mar 24 results solution
11 Mar 9 Quantified Boolean Formulas. 11 slides        
12 Mar 10 Quantified Boolean Formulas. 11 slides        
13 Mar 16 Satisfiability Checking for QBF. 11 slides        
14 Mar 17 Satisfiability Checking for QBF. 11 slides pdf file Apr 28 results solution
15 Mar 23 Propositional Logic of Finite Domains. 12 slides        
16 Mar 24 Transition Systems and Temporal Properties. 13 slides pdf file May 12 results solution
17 Mar 30 Transition Systems and Temporal Properties. Kripke Structures 13, 14 slides        
18 Mar 31 LTL 14 slides        
19 Apr 27 LTL 14 slides        
20 Apr 28 LTL 14 slides        
21 May 4 LTL 14 slides        
22 May 5 Model Checking 15 slides        
23 May 26 Revision Session Room 1.3, 15:00