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.

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.

# | 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 | -- |

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 |

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 |