| Settimana | Argomento | Martedì (ore 14:00:-15:30) | Mercoledì (ore 14:00-17:20) |
| 1:02-08mar | FOL e Query Congiuntive | Lezioni 1,2 |
Lezioni 3-6 |
| 2:09-15mar | Formalizzazione dei Diagrammi delle classi UML | Lezioni
7,8 - Il teorema di Chandra-Merlin - Contenimento tra query congiuntive - Unioni di query congiuntive (query positive) |
Lezioni 9-12 |
| 3:16-22mar | Formalizzazione dei Diagrammi delle classi UML | Lezione annullata | Lezione annullata |
| 4:23-29mar | Formalizzazione dei Diagrammi delle classi UML | Lezioni 13-14 - Formalizzazione dei diagrammi delle classi in FOL |
Lezioni 15-18 |
| 5:30mar-5apr | Formalizzazione dei Diagrammi delle classi UML | Lezioni 19-20 - Tableaux per basi di conoscenza ALC - EXPTIME Hardness del ragionamento su diagrammi UML |
Lezioni 21-24 |
| 6:6mar-12apr | Formalizzazione dei Diagrammi delle classi UML | Lezioni 25-26 |
Vacanze Pasqua |
| 7:13mar-19apr | Interrogazioni su Diagrammi delle classi UML | Vacanze Pasqua
|
Lezioni 27-30 |
| 8:20-26apr | Interrogazioni su Diagrammi delle classi UML |
Lezioni 31,32 - Query epistemiche |
Lezioni 33-36 |
| 9:27apr-03mag | Pre/Postcondizioni nei programmi | Lezioni 37,38 - Hoare Logic |
Lezioni 39,42 |
| 10:04-10mag | Model checking | Lezioni 43,44 - Introduzione al model checking |
Lezioni 45,48 |
| 11:11-17mag | Model checking | Lezioni 49,50 - Model checking in CTL: valutazione della formula sul transition system |
Lezioni 51,54 (Fabio Patrizi) |
| 12:18-24mag | Model checking | Lezioni 55,56 (Fabio Patrizi) - OBDDs |
Lezioni 57,58 (Fabio Patrizi) |
| 13:25-31mag | Model checking | Lezioni 59,60 - LTL - Automi di Buchi su stringhe infinite - Model checking in LTL: manipolazione di automi di Buchi |
Lezioni 61,64 |