Diario delle Lezioni 2021-2022

Calendario delle lezioni

Lezioni lunedì e giovedì ore 11-14 a partire dal 4 aprile 2022 sul canale Microsoft Teams

Settimana n.1

• lezione #1: Lunedì 4 Aprile, presentazione del corso. La Deduzione Naturale (Gentzen, 1935 e Prawitz, 1965): il frammento minimale. Riferimenti: capitoli 1 e 2 di Proofs and Types. 

• lezione #2: Giovedì 7 Aprile, La Deduzione Naturale: il frammento intuizionista. Riferimenti: capitoli 1, 2 e 10 (solo da pag. 72 a 79) di Proofs and Types.

scarica le slides delle lezioni.

Settimana n.2

• Lezione #3: Lunedì 11 Aprile, il Calcolo dei Sequenti di Gentzen per la Logica Intuizionista (LJ). Riferimenti: capitolo 5 (da pag. 28 a 38) di Proofs and Types. Scarica le slides della lezione. Vedi anche altre slides su LJ.

• lezione #4: Giovedì 14 Aprile, il Teorema dell'Eliminazione delle regole del Taglio per LK (LJ) e Proprietà della Sottoformula. Versione moltiplicativa ed Additiva delle regole logiche ed equivalenza delle due formulazioni. Riferimenti: capitoli 13 (da pag. 104 a pag. 110) di Proofs and Types. Scarica le slides ulle eliminazione del taglio per KK nella formulazione ad una sola parte ed a due parti . Vedi anche altre slides su LK(LJ).

Settimana n.3

• lezione Lunedì 18 Aprile (annullata per le festività Pasquali)

• lezione #5: Giovedì 21 Aprile, introduzione alla Logica Lineare, le regole del calcolo dei sequenti ad una parte. Riferimenti, Capitolo1, da pag 9 a pag 22, dell'Handbook of Linear Logic (versione Gennaio 2022). Svolgere gli esercizi di pag. 15 e pag 16.

Settimana n.4

• lezione Lunedì 25 Aprile (annullata per le festa della Liberazione)

• lezione #6: Giovedì 28 Aprile, Il teorema di eliminazione dei tagli per la logica lineare (proposizionale), Capitolo1, pagg. 23-32 dell'Handbook of Linear Logic (versione Gennaio 2022). Scarica le slides della lezione.

Settimana n.5

• lezione #7: Lunedì 2 Maggio, il frammento moltiplicativo puro (MLL) della logica lineare; le nozioni di proof-structure e proof-net; il criterio di correttezza di Danos e Regnier (ACC) Riferimenti: pgg 41-48 del Capitolo 2 dell'Handbook of Linear Logic.

• lezione #8: Giovedì 5 Maggio: Teorema di De-sequenzializzazione delle prove di MLL, Teorema di Splitting e Teorema di Sequenzializzazione delle proof net di MLL; definzione dei passi di riduzione sulle proof net: terminazione e confluenza (unicità della forma normale). Riferimenti: pgg 48-52 del Capitolo 2 dell'Handbook of Linear Logic.

Settimana n.6

• lezione #9: Lunedì 9 Maggio: Regole di cut-reduction per le reti di MLL e stabilità del criterio di correttzza DR (ACC) sotto le regole di riduzione del taglio. Il criterio di correttezza Contrattile di Danos per le rei di MLL ed equivalenza con il criterio DR (ACC). Discussione della complessità del criterio di DR e del criterio contrattile: Riferimenti: Capitolo 2 dell'Handbook e  (un frammento della) Tesi di Vincent Danos sulla contrazione.

• lezione #10: Giovedì 12 Maggio: la proprietà di focalizzazione di Andreoli per le dimostrazioni di MLL. Riferimenti: articolo Andreoli-Maieli sulla focalizzazione. Il concetto di modulo per le reti moltiplicative. Riferimenti: articolo Modularity of proof nets: generating the type of a module.

Settimana n.7

• lezione #11 (Maieli): Lunedì 16 Maggio ore 11-14 aula 8. il frammento moltiplicativo-additivo puro (MALL) della logica lineare; il Criterio di Correttezza delle strutture dimostrative con pesi monomialli. Riferimenti: Cut Elimination for Monomial Proof Nets of the Purely Multiplicative and Additive Fragment of Linear Logic.

• lezione #12 (Tortora de Falco): Mercoledì 18 ore 17-20 in aula 6, una introduzione alla Logica Lineare e semantica delle sue dimostrazioni. Scarica le dispense.

• lezione #13 (Maieli): Giovedì 19 Maggio ore 11-14 aula 8: le reti moltiplicative con le unità e le reti moltiplicative-esponenziali (MELL). Riferimenti cap. 2.3  dell'Handbook of Linear Logic.

• lezione #14 (Tortora de Falco): Giovedì 19 Maggio ore 17-20 in aula 6,  una introduzione alla Logica Lineare e semantica delle sue dimostrazioni. Scarica le dispense.

Fine del corso