Embedded Files
Le lezioni si terranno ogni Martedì e Giovedì dalle ore 17 alle ore 20 in Aula 6 (via Ostiense 236)
1° Settimana
Lezione 1 (martedì 8 aprile ore 17-20) 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.
Lezione 2 (giovedì 10 aprile ore 17-20) 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.
2° Settimana
Lezione 3 (martedì 15 aprile ore 17-20) 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.
Lezione 4 (giovedì 17 aprile ore 17-120) 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.
3° Settimana
Lezione 5 (martedì 29 aprile ore 17-20) 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.
4° Settimana
Lezione 6 (martedì 6 maggio ore 17-20) 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.
Lezione 7 (giovedì 8 maggio ore 17-20) 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.
5° Settimana
Lezione 8 (martedì 13 maggio ore 17-20) 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
Lezione 9 (giovedì 15 maggio ore 17-20) Regole di cut-reduction per le reti di MLL e stabilità del criterio di correttezza Danos-Regnier (ACC) sotto le regole di riduzione del taglio.
6° Settimana
Lezione 10 (martedì 20 maggio ore 17-20) Il criterio di correttezza contrattile (CC) di Danos, equivalenza con i criterio ACC e stabilità dle 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à.
Lezione 11 (giovedì 22 maggio ore 17-20) La proprietà di focalizzazione delle dimostrazioni della logica lineare.
7° Settimana
Lezione 12 (martedì 27 maggio ore 17-20) Introduzione alle Reti di MELL.
Lezione extra (giovedì 29 maggio ore 17-20): introduzione alle reti dimostrative di MALL
AVVISI
AVVISI
Seminari di Logica: Martedì 3 Giugno ore 10 stanza riunioni n. 71 (Via della Vasca Navale, 84)
Prova scritta: Lunedì 9 Giugno ore 11-14 aula A (Via della Vasca Navale, 84).
Alcune letture consigliate (PDF disponibili qui)
G. Gentzen. Proof of Normalization for Natural Deduction.
François Métayer, Homology of proof-nets
CHRISTIAN RETORE, A semantic characterisation of the correctness of a proof net
Stefano Guerrini. A linear algorithm for MLL proof net correctness and sequentialization
Dominic J. D. Hughes Land Willem B. Heijltjes. Conflict nets: Efficient locally canonical MALL proof nets
Jean-Marc Andreoli and Laurent Mazaré. Concurrent Construction of Proof-Nets
Page updated
Google Sites
Report abuse