Logic in Computer Science

General Information

This course is intended as an introduction to computational logic, its main notions and methods, applications and modelling.

Assessment

20% of the assessment for this course will come from assessed exercises. The exercises will be published on this page before lectures on Fridays or earlier. The deadline for each exercise will be the next Friday, 4pm.

News

(13/01/2010) Solution to Exercise 11 added
(11/01/2010) Exercise 11 (just for exam revision) and Solution to Exercise 10 added
(29/10/2009) Part of exercise 4 has been moved to exercise 5.
(29/10/2009) Solutions to exercises and typical errors have been added.
(04/10/2009) This page has been created.

Timetable

# date topic slides chapters assignment deadline
1 Oct 01 Introduction slides 3
2 Oct 02 Propositional Logic: syntax and semantics. slides 3 1 Oct 09
3 Oct 08 Formula evaluation. Satisfiability slides 3, 4
4 Oct 09 CNF slides 5 2 Oct 16
5 Oct 15 Positions and polarity slides 4, 5
6 Oct 16 DPLL slides 5 3 Oct 22
7 Oct 22 Random clause generation slides 8
8 Oct 23 Randomised algorithms for satisfiability checking slides 8 4 Oct 29
9 Oct 29 Randomised algorithms for satisfiability checking. Semantic Tableaux slides 8, 9 5 Nov 12
10 Oct 30 Binary Decision Diagrams slides 10
11 Nov 12 Binary Decision Diagrams slides 10 6 Nov 19
12 Nov 13 Binary Decision Diagrams. Quantified Boolean Formulas slides 10, 11
13 Nov 19 Quantified Boolean Formulas slides 11 7 Nov 26
14 Nov 20 Quantified Boolean Formulas slides 11
15 Nov 26 Quantified Boolean Formulas slides 11 8 Dec 03
16 Nov 27 Propositional Logic of Finite Domains slides 12
17 Dec 03 Transition Systems slides 13
18 Dec 04 Transition Systems slides 13 9 Dec 10
19 Dec 10 LTL slides 14 10 Dec 17
20 Dec 11 LTL slides 14
21 Dec 17 Model Checking slides
22 Dec 18 Model Checking slides

List of Assignments

Assignment deadline solution
all --- all
1 Oct 09 1
2 Oct 16 2
3 Oct 22 3
4 Oct 29 4
5 Nov 12 5
6 Nov 19 6
7 Nov 26 7
8 Dec 03 8
9 Dec 10 9
10 Dec 17 10
11 Jan 11 11

List of Slides

topic/link to slides last modified
All slides Dec 18
Introduction Oct 04
Propositional Logic Oct 04
Satisfiability Oct 08
DPLL Oct 30
Satisfiability and Randomisation Oct 23
Semantic Tableaux Oct 29
Binary Decision Diagrams Nov 13
Quantified Boolean Formulas Nov 25
Propositional Logic of Finite Domains Nov 27
Transition Systems Dec 03
LTL Dec 18
Model Checking Dec 18