Logic and Modeling 2010
Note that this is the last year Web page! Click here to access the 2011 Web page!
General Information
This course is intended as an introduction to computational logic, its main notions and methods, applications and modelling.
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, 4pm.
Previous Year Web Pages
News
(05/11/2010) Exercise 5: the deadline was moved one week
forward due to the reading week.
Timetable
| # | date | topic | slides | chapters | assignment | deadline |
| 1 | Sep 30 | Introduction | slides | 2, 3 | ||
| 2 | Oct 01 | Propositional Logic: Syntax and Semantics. | slides | 3 | 1 | Oct 08 |
| 3 | Oct 07 | Propositional Logic: Semantics. Satisfiability | slides | 3, 4 | ||
| 4 | Oct 08 | Splitting. CNF | slides | 4, 5 | 2 | Oct 15 |
| 5 | Oct 14 | CNF | slides | 4, 5 | ||
| 6 | Oct 15 | DPLL | slides | 5 | 3 | Oct 22 |
| 7 | Oct 21 | Encoding Problems in SAT | slides | |||
| 8 | Oct 22 | Properties of randomly generated clause sets | slides | 8 | 4 | Oct 29 |
| 9 | Oct 28 | Randomised algorithms for satisfiability checking | slides | 8 | ||
| 10 | Oct 29 | Semantic Tableaux | slides | 9 | 5 | Nov 12 |
| 11 | Nov 11 | Binary Decision Diagrams | slides | 10 | ||
| 12 | Nov 12 | Binary Decision Diagrams. | slides | 10 | 6 | Nov 19 |
| 13 | Nov 18 | Quantified Boolean Formulas | slides | 11 | ||
| 14 | Nov 19 | Quantified Boolean Formulas | slides | 11 | 7 | Nov 26 |
| 15 | Nov 25 | Quantified Boolean Formulas | slides | 11 | ||
| 16 | Nov 26 | Quantified Boolean Formulas. Modelling in logic | slides | 11, 12 | 8 | Dec 03 |
| 17 | Dec 02 | Propositional Logic of Finite Domains | slides | 12 | ||
| 18 | Dec 03 | Transition Systems | slides | 13 | 9 | Dec 10 |
| 19 | Dec 09 | LTL | slides | 14 | ||
| 20 | Dec 10 | LTL | slides | 14 | 10 | Dec 17 |
| 21 | Dec 16 | Model Checking | slides | |||
| 22 | Dec 17 | Model Checking | slides |
List of Assignments
| Assignment | deadline | solution |
| all | --- | all |
| 1 | Oct 08 | 1 |
| 2 | Oct 15 | 2 |
| 3 | Oct 22 | 3 |
| 4 | Oct 29 | 4 |
| 5 | Nov 12 | 5 |
| 6 | Nov 19 | 6 |
| 7 | Nov 26 | 7 |
| 8 | Dec 03 | 8 |
| 9 | Dec 10 | 9 |
| 10 | Dec 17 | 10 |
| 11 | -- | 11 |
List of Slides
| topic/link to slides | last modified |
| All slides | Dec 16 |
| Introduction | Oct 01 |
| Propositional Logic | Oct 08 |
| Satisfiability | Oct 08 |
| DPLL | Oct 15 |
| Encoding Problems in SAT | Oct 21 |
| Satisfiability and Randomisation | Oct 28 |
| Semantic Tableaux | Oct 29 |
| Binary Decision Diagrams | Nov 15 |
| Quantified Boolean Formulas | Nov 27 |
| Propositional Logic of Finite Domains | Dec 02 |
| Transition Systems | Dec 07 |
| LTL | Dec 16 |
| Model Checking | Dec 16 |