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 |