Logic in Computer Science
Note that this Web page is under development. I will be adding more information gradually.
This course is intended as an introduction to computational logic, its main notions and methods, applications and modelling.
News
(23/05/2008) Revision lecture rescheduled.
There is a change in the revision lecture schedule (by mistake,
it fell on a bank holiday).
The revision lecture is now scheduled for Tuesday, May 27th,
10am, room 2.15 of Kilburn Building. (23/05/2008) Exercises with solutions.
A large collection of
exercises with solutions is now
available here. (20/02/2008) This page was created.
Timetable
| # | date | topic | slides | chapters | assignment | deadline |
| 1 | Jan 31 | Introduction | slides | |||
| 2 | Feb 1 | Propositional Logic: syntax and semantics. | slides | 3 | ||
| 3 | Feb 7 | Formula evaluation. Satisfiability | slides | 3, 4 | 1 | Feb 14 |
| 4 | Feb 8 | Splitting. Monotonicity | slides | 4 | ||
| 5 | Feb 14 | Polarity and monotonicity. Clauses and CNF | slides | 4, 5 | 2 | Feb 22 |
| 6 | Feb 15 | Naming. Unit propagation | slides | 5 | ||
| 7 | Feb 21 | Optimised naming. DLL. Random clause generation | slides | 5, 8 | ||
| 8 | Feb 22 | Randomised algorithms for satisfiability checking | slides | 8 | 3 | Feb 29 |
| 9 | Feb 28 | Semantic Tableaux. BDDs | slides | 9, 10 | 4 | Mar 7 |
| 10 | Feb 29 | BDDs | slides | 10 | ||
| 11 | Mar 6 | BDDs. Quantified Boolean Formulas | slides | 10, 11 | ||
| 12 | Mar 7 | Quantified Boolean Formulas | slides | 11 | 5 | Mar 14 |
| 13 | Mar 13 | Quantified Boolean Formulas | slides | 11 | ||
| 14 | Mar 14 | Quantified Boolean Formulas | slides | 11 | ||
| 15 | Apr 10 | Quantified Boolean Formulas | slides | 11 | 6 | Apr 18 |
| 16 | Apr 11 | Propositional Logic of Finite Domains | slides | 12 | ||
| 17 | Apr 17 | Transition Systems and Temporal Propeties | slides | 13 | ||
| 18 | Apr 18 | Transition Systems and Temporal Propeties. LTL | slides | 13, 14 | ||
| 19 | Apr 24 | LTL | slides | 14 | ||
| 20 | Apr 25 | LTL | slides | 14 | 7 | May 2 |
| 21 | May 1 | Model Checking | slides |