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:

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.
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.

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.
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.

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.
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.

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.
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

Page updated

Google Sites

Report abuse