1.  lunedì 12 aprile: presentazione del corso. La Deduzione Naturale (Gentzen, 1935 e Prawitz, 1965): il frammento minimale. Riferimenti: capitoli 1 e 2 di Proofs and Types. Scarica le slides della lezione.

2. giovedì 15 aprile: La Deduzione Naturale: il frammento intuizionista. Riferimenti: capitoli 1, 2 e 10 (solo da pag. 72 a 79) di Proofs and Types.

3. lunedì 19 aprile: il Calcolo dei Sequenti di Gentzen per la Logica Intuizionista (LJ) e per la Logica Classica (LK). Riferimenti: capitolo 5 (da pag. 28 a 38) di Proofs and Types. Scarica le slides della lezione. Vedi anche altre slides su LK(LJ).

4. giovedì 22 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 della lezione (e maggiori dettagli tecnici della prova). Vedi anche altre slides su LK(LJ).

5. lunedì 26 aprile: introduzione alla Logica Lineare, le regole del calcolo dei sequenti a due parti; l'eta espansione degli axiomi. Riferimenti, capitolo 3 (da pag.15 a pag. 19) dell'Handbook of Linear Logic. Scarica le slides della lezione.

6. giovedì 29 aprile: introduzione alla Logica Lineare; le leggi di De Morgan della negazione lineare, l'involutività della negazione lineare, le regole del calcolo ad una sola parte; equivalenza delle due formulazioni del calcolo. Riferimenti, capitolo 3 (da pag.20 a pag. 35) dell'Handbook of Linear Logic. Scarica le slides della lezione.

7. lunedì 3 maggio: il frammento moltiplicativo puro (MLL) della logica lineare; le nozioni di proof-structure e proof-net; il criterio di correttezza (ACC) e l'eliminazione del taglio. Riferimenti: capitolo 4 (proof nets) dell'Handbook of Linear Logic. Scarica le slides della lezione.

8. giovedì 6 maggio: il frammento moltiplicativo puro (MLL) della logica lineare; Sequenzializzazione delle reti moltiplicative (Lemma di Splitting). Eliminazione dei tagli delle reti moltiplicative: terminazione, confluenza e stabilità della correttezza sotto riduzione. Riferimenti: capitolo 4 (proof nets) dell'Handbook of Linear Logic + slides introduttive. Scarica le slides della lezione.

9. lunedì 10 maggio: il frammento moltiplicativo puro (MLL) della logica lineare; il Criterio di Contrazione delle Reti e la Proprietà di Focalizzazione per la ricerca delle dimostrazioni. Riferimenti: (frammento della) Tesi di Vincent Danos sulla contrazione + articolo Andreoli-Maieli sulla focalizzazione. Scarica le slides della lezione.

10. giovedì13 maggio: esercitazione e discussione di alcuni temi affrontati a lezione.

11. lunedì 17 maggio: il frammento moltiplicativo-additivo puro (MALL) della logica lineare; il Criterio di Correttezza delle strutture dimostrative con pesi monomialli. Riferimenti: articolo R. Maieli, Cut Elimination for Monomial Proof Nets of the Purely Multiplicative and Additive Fragment of Linear Logic. Scarica le slides della lezione.

12. giovedì 20 maggio: il frammento moltiplicativo-additivo puro (MALL) della logica lineare; l'eliminazione dei tagli. Riferimenti: articolo R. Maieli, Cut Elimination for Monomial Proof Nets of the Purely Multiplicative and Additive Fragment of Linear Logic. Qualche cenno al frammento puro Moltiplicativo ed Esponenziale della logica lineare (MELL). Scarica le slides (D.Mazza) Attack of the Exponentials.

13. lunedì 24 maggio: introduzione alla semantica denotazionale della logica lineare a cura del prof. Lorenzo Tortora de Falco. Gli spazi coerenti per il frammento MLL. Riferimenti: pag-57-60 di J.-Y. Girard,  Linear Logic  ; C. Retoré, On the relation between coherence semantics and multiplicative proof nets. Michele Pagani ”Proofs, Denotational Semantics and Observational Equivalences in Multiplicative Linear Logic”. Note sulla semantica denotazionale delle strutture di prova a cura di Lorenzo Tortora de Falco.

Fine del corso.