Logic and Modeling 2013

General Information

This course is intended as an introduction to computational logic, its main notions and methods, applications and modelling. This page is the main source of information and news about the course.

The course will consist of 22 lectures. After each lecture the slides for this lecture will be available online from this page. You should attend the lectures to understand the material.

I am not using any textbook for this course and a substantial part of the material I present cannot be found in textbooks at all. Moreover, these is no single textbook that would cover a large part of this material. There will be some reading material provided for your convenience in the "chapters" section below, however you should be aware that its quality varies and it is especially patchy at its coverage of the last lectures. I will try to update some chapters, yet lectures and slides will remain the main source of information. Therefore, I advise you to attend lectures and make your notes during them.

The reading material has an index, also included here. If you forgot some notions or notation, please check the index! The index will be updated each time when new chapters are added.

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, 3:00pm. Why not later? I do not want students to solve exercises during my lectures, so the solutions must be handed in before the lecture.

I will try to put model solutions for each exercise online soon after the deadline for this exercise. It also means that it makes no sense for you to ask for a personal deadline extension.

News

Timetable

# date topic slides chapters exercise deadline
1 Sep 26 Introduction slides 2
2 Sep 27 Propositional Logic: Syntax and Semantics. slides 3 1 Oct 04
3 Oct 03 Formula Evaluation. Satisfiability slides 3, 4
4 Oct 04 Satisfiability slides 4 2 Oct 11
5 Oct 10 CNF slides 5
6 Oct 11 Definitional clause form transformation. Encoding problems in SAT slides 5 3 Oct 18
7 Oct 17 DPLL slides 5
8 Oct 18 Properties of randomly generated clause sets slides 8 4 Oct 25
9 Oct 24 Randomised algorithms for satisfiability checking slides 8
10 Oct 25 Semantic Tableaux slides 9 5 Nov 8
11 Nov 07 Binary Decision Diagrams slides 10
12 Nov 08 Binary Decision Diagrams. slides 10 6 Nov 15
13 Nov 14 Quantified Boolean Formulas slides 11
14 Nov 15 Quantified Boolean Formulas slides 11 7 Nov 22
15 Nov 21 Quantified Boolean Formulas slides 11
16 Nov 22 Propositional Logic of Finite Domains slides 12 8 Nov 29
17 Nov 28 Transition Systems slides 13
18 Nov 29 Transition Systems. LTL slides 13 9 Dec 06
19 Dec 05 LTL slides 14
20 Dec 06 LTL slides 14 10 Dec 13
21 Dec 12 Model Checking slides
22 Dec 13 Model Checking slides 11 --

List of Assessed Exercises

exercise deadline solution
1 Oct 04 1
2 Oct 11 2
3 Oct 18 3
4 Oct 25 4
5 Nov 08 5
6 Nov 15 6
7 Nov 22 7
8 Nov 29 8
9 Dec 06 9
10 Dec 13 10
11 -- 11

List of Slides

topic/link to slides last modified
All slides Jan 16
Introduction Sep 30
Propositional Logic Oct 03
Satisfiability Oct 04
DPLL Oct 17
Satisfiability and Randomisation Oct 24
Semantic Tableaux Nov 3
Binary Decision Diagrams Nov 12
Quantified Boolean Formulas Nov 22
Propositional Logic of Finite Domains Nov 22
Transition Systems Dec 01
LTL Dec 07
Model Checking Jan 16