Logic and Modeling 2011
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, 4:30pm.
I will try to put model solutions of each exercises 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.
Previous Year Web Pages
The course will be similar (but not identical!) to the last year course. You are welcome to check the previous year Web page of this course, for example, if you prefer to read the content in advance.
News
Timetable
| # | date | topic | slides | chapters | exercise | deadline |
| 1 | Sep 29 | Introduction | slides | 2, 3 | ||
| 2 | Sep 30 | Propositional Logic: Syntax and Semantics. | slides | 3 | 1 | Oct 07 |
| 3 | Oct 06 | Formula Evaluation. Satisfiability | slides | 3, 4 | ||
| 4 | Oct 07 | Satisfiability | slides | 4 | 2 | Oct 14 |
| 5 | Oct 13 | CNF | slides | 5 | ||
| 6 | Oct 14 | Definitional clause form transformation. Encoding problems in SAT | slides | 5 | 3 | Oct 21 |
| 7 | Oct 20 | DPLL | slides | 5 | ||
| 8 | Oct 21 | Properties of randomly generated clause sets | slides | 8 | 4 | Oct 28 |
| 9 | Oct 27 | Randomised algorithms for satisfiability checking | slides | 8 | ||
| 10 | Oct 28 | Semantic Tableaux | slides | 9 | 5 | Nov 15 |
| 11 | Nov 10 | Binary Decision Diagrams | slides | 10 | ||
| 12 | Nov 11 | Binary Decision Diagrams. | slides | 10 | 6 | Nov 18 |
| 13 | Nov 17 | Quantified Boolean Formulas | slides | 11 | ||
| 14 | Nov 18 | Quantified Boolean Formulas | slides | 11 | 7 | Nov 25 |
| 15 | Nov 24 | Quantified Boolean Formulas | slides | 11 | ||
| 16 | Nov 25 | Propositional Logic of Finite Domains | slides | 12 | 8 | Dec 05 |
| 17 | Dec 01 | Transition Systems | slides | 13 | ||
| 18 | Dec 02 | Transition Systems | slides | 13 | 9 | Dec 14 |
| 19 | Dec 08 | LTL | slides | 14 | ||
| 20 | Dec 09 | LTL | slides | 14 | 10 | Dec 16 |
| 21 | Dec 15 | Model Checking | slides | |||
| 22 | Dec 16 | Model Checking | slides |
List of Assessed Exercises
| exercise | deadline | solution | solution (with animation) |
| all | --- | all | all |
| 1 | Oct 07 | 1 | 1 |
| 2 | Oct 14 | 2 | 2 |
| 3 | Oct 21 | 3 | 3 |
| 4 | Oct 28 | 4 | 4 |
| 5 | Nov 15 | 5 | 5 |
| 6 | Nov 18 | 6 | 6 |
| 7 | Nov 25 | 7 | 7 |
| 8 | Dec 05 | 8 | 8 |
| 9 | Dec 14 | 9 | 9 |
| 10 | Dec 16 | 10 | 10 |
List of Slides
| topic/link to slides | last modified |
| All slides | Jan 12 |
| Introduction | Sep 30 |
| Propositional Logic | Oct 06 |
| Satisfiability | Oct 07 |
| DPLL | Oct 21 |
| Satisfiability and Randomisation | Nov 17 |
| Semantic Tableaux | Nov 1 |
| Binary Decision Diagrams | Nov 12 |
| Quantified Boolean Formulas | Nov 25 |
| Propositional Logic of Finite Domains | Nov 25 |
| Transition Systems | Dec 05 |
| LTL | Dec 13 |
| Model Checking | Jan 12 |
Reading Material by Subject
| # | Chapter | last modified |
| All chapters | Oct 06 | |
| 2 | Preliminaries | Oct 06 |
| Index | Oct 06 |