Logic and Modeling 2014

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

List of Assessed Exercises

Exercise Deadline Solution
1 Oct 03 1
2 Oct 10 2
3 Oct 17 3
4 Oct 24 4
5 Nov 07 5
6 Nov 14 6
7 Nov 21 7
8 Nov 28 8
9 Dec 05 9
10 Dec 12 10

List of Slides

Topic/Link to slides Last modified
Introduction Oct 02
Propositional Logic Oct 04
Satisfiability Oct 04
DPLL Oct 17
Satisfiability and Randomisation Nov 4
Semantic Tableaux Nov 4
Binary Decision Diagrams Nov 12
Quantified Boolean Formulas Nov 25
Propositional Logic of Finite Domains Nov 25
Transition Systems Nov 29
LTL Dec 08
Model Checking Jan 06

Reading Material by Subject

# Chapter Last modified
Preliminaries 2 Sep 27
Propositional Logic 3 Sep 27
Satisfiability 4 Sep 27
DPLL 5 Sep 27
Satisfiability and Randomisation 8 Sep 27
Semantic Tableaux 9 Sep 27
Binary Decision Diagrams 10 Sep 27
Quantified Boolean Formulas 11 Sep 27
Propositional Logic of Finite Domains 12 Sep 27
Transition Systems 13 Sep 27
LTL 14 Sep 27
Model Checking 15 Sep 27