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 |