Edizione 2025-26

Le lezioni dell'a.a. 2025-2026 si terrano nel secondo semestre con inizio il 14 Aprile e termineranno a fine maggio. 

Le lezioni si terranno ogni martedì (in Aula 4) e giovedì (in Aula 8) dalle ore 17 alle ore 20 in Via Ostiense 234.

Calendario delle lezioni:

1. Martedì 14 Aprile ore 17-20 (aula 4, Via Ostiense 234): Presentazione del corso. I sistemi assiomatici "à la Hilbert". La Deduzione Naturale di Gentzen (1935): il frammento minimale. Riferimenti: capitoli 1 e 2 di Proofs and Types.

2. Giovedì 16 Aprile ore 17-20 (aula C006, palazzina C, Largo Murialdo): La Deduzione Naturale: il frammento intuizionista (completo senza quantificatori). I problemi legati alla Normalizzazione ed alla Proprietà della Sottoformula. Le deduzioni in forma canonica. Esempi ed esercizi. Riferimenti: capitoli 1, 2 e 10 (pagg. 72 - 79) di Proofs and Types.

3. Martedì 21 Aprile ore 17-20  (aula C006, palazzina C, Largo Murialdo): Dal Calcolo della Deduzione Intuizionita (NJ) al Calcolo dei Sequenti Intuizionisti (LJ). Limiti espressivi di LJ: la dimostrazione della equivalenza della Reductio ad Absurdum (RAA) e del Principio del Terzo Escluso. Il problema della Canonicità delle dimostrazioni.

4. Giovedì 23 Aprile ore 17-20  (aula C006, palazzina C, Largo Murialdo): 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. 

5. Martedì 28 Aprile ore 17-20  (aula C006, palazzina C, Largo Murialdo): 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  Svolgere gli esercizi di pag. 15 e pag 16.   

6. Giovedì 30 Aprile ore 17-20 (aula C208)  Il teorema di eliminazione dei tagli per la logica lineare (proposizionale), Capitolo1, pagg. 23-32 dell'Handbook of Linear Logic. Le slides della lezione sono disponibil qui.

7. Martedì 5 Maggio ore 17-20  (aula C006, palazzina C, Largo Murialdo): 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 ed articolo di V. Danos and L. Regnier, The structure of Multiplicatives.

8. Giovedì 7 Maggio ore 17-20  (aula C006, palazzina C, Largo Murialdo): Correttezza (Teorema di de-sequenzializzazione) e Completezza (Teorema di Sequenzializzazione) del Criterio di Correttezza delle Strutture di Prova di di MLL (Teorema di de-sequenzializzazione,  Splitting Lemma  e Teorema di Sequenzializzazione). Riferimenti: pgg 46-63 del Capitolo 2 dell' Handbook of Linear Logic ed articolo di O. Laurent, Sequentialization of Multiplicative Proof Nets

9. Martedì 12 Maggio ore 17-20  (aula C006, palazzina C, Largo Murialdo): Il criterio di correttezza contrattile (CC) di Vincent Danos, equivalenza con i criterio ACC e stabilità del criterio CC sotto le regole di cut reductions. Complessità in tempo dei criteri di correttezza. Riferimenti: pgg 51-54 del Capitolo 2 dell' Handbook of Linear Logic. Lettura consigliata: S. Guerrini, A linear algorithm for MLL proof net correctness and sequentialization.Il frammento MLL con le Unità.

10. Giovedì 14 Maggio ore 17-20  (aula C006, palazzina C, Largo Murialdo): Le reti di prova per il frammento moltiplicativo con le unità. La proprietà di focalizzazione delle dimostrazioni della logica lineare. Moduli moltiplicativi.

11. Martedì 19 Maggio ore 17-20  (aula C006, palazzina C, Largo Murialdo): introduzione alle reti dimostrative di MALL. Letture consigliate: 

• R. Maieli, Cut Elimination for Monomial Proof Nets of the Purely Multiplicative and Additive Fragment of Linear Logic

• Retractile Proof Nets of the Purely Multiplicative and Additive Fragment of Linear Logic.  R. Maieli

• Conflict Nets for MALL: Dominic Hughes and Willem Heijltjes

• Proof Nets for Unit-Free Multiplicative-Additive Linear Logic, DOMINIC J. D. HUGHES and ROB J. VAN GLABBEEK 

12. Giovedì 21 Maggio ore 17-20 (aula C006): Introduzione alle Reti di MELL. Riferimenti: D. Mazza, Attack of the Exponentials. Parsing MLL Proof Nets,  Stefano Guerrini and Andrea Masini

13. Martedì 26 Maggio ore 14-17 in streamig (aula M2)

14. Giovedì 28 Maggio ore 14-17 aula B (Vasca Navale)