Logic in Computer Science
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.
News
(13/01/2010) Solution to Exercise 11 added
(11/01/2010) Exercise 11 (just for exam revision) and Solution to Exercise 10 added
(29/10/2009) Part of exercise 4 has been moved to exercise 5.
(29/10/2009) Solutions to exercises and typical errors have been added.
(04/10/2009) This page has been created.
Timetable
| # | date | topic | slides | chapters | assignment | deadline |
| 1 | Oct 01 | Introduction | slides | 3 | ||
| 2 | Oct 02 | Propositional Logic: syntax and semantics. | slides | 3 | 1 | Oct 09 |
| 3 | Oct 08 | Formula evaluation. Satisfiability | slides | 3, 4 | ||
| 4 | Oct 09 | CNF | slides | 5 | 2 | Oct 16 |
| 5 | Oct 15 | Positions and polarity | slides | 4, 5 | ||
| 6 | Oct 16 | DPLL | slides | 5 | 3 | Oct 22 |
| 7 | Oct 22 | Random clause generation | slides | 8 | ||
| 8 | Oct 23 | Randomised algorithms for satisfiability checking | slides | 8 | 4 | Oct 29 |
| 9 | Oct 29 | Randomised algorithms for satisfiability checking. Semantic Tableaux | slides | 8, 9 | 5 | Nov 12 |
| 10 | Oct 30 | Binary Decision Diagrams | slides | 10 | ||
| 11 | Nov 12 | Binary Decision Diagrams | slides | 10 | 6 | Nov 19 |
| 12 | Nov 13 | Binary Decision Diagrams. Quantified Boolean Formulas | slides | 10, 11 | ||
| 13 | Nov 19 | Quantified Boolean Formulas | slides | 11 | 7 | Nov 26 |
| 14 | Nov 20 | Quantified Boolean Formulas | slides | 11 | ||
| 15 | Nov 26 | Quantified Boolean Formulas | slides | 11 | 8 | Dec 03 |
| 16 | Nov 27 | Propositional Logic of Finite Domains | slides | 12 | ||
| 17 | Dec 03 | Transition Systems | slides | 13 | ||
| 18 | Dec 04 | Transition Systems | slides | 13 | 9 | Dec 10 |
| 19 | Dec 10 | LTL | slides | 14 | 10 | Dec 17 |
| 20 | Dec 11 | LTL | slides | 14 | ||
| 21 | Dec 17 | Model Checking | slides | |||
| 22 | Dec 18 | Model Checking | slides |
List of Assignments
| Assignment | deadline | solution |
| all | --- | all |
| 1 | Oct 09 | 1 |
| 2 | Oct 16 | 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 | Jan 11 | 11 |
List of Slides
| topic/link to slides | last modified |
| All slides | Dec 18 |
| Introduction | Oct 04 |
| Propositional Logic | Oct 04 |
| Satisfiability | Oct 08 |
| DPLL | Oct 30 |
| Satisfiability and Randomisation | Oct 23 |
| Semantic Tableaux | Oct 29 |
| Binary Decision Diagrams | Nov 13 |
| Quantified Boolean Formulas | Nov 25 |
| Propositional Logic of Finite Domains | Nov 27 |
| Transition Systems | Dec 03 |
| LTL | Dec 18 |
| Model Checking | Dec 18 |