Primo appello febbraio 2010 Testo
della parte di logica con soluzioni e commenti.
Secondo appello febbraio 2010 Testo
della parte di logica con alcune soluzioni.
Primo appello giugno 2010 Testo
della parte di logica con soluzioni e commenti dettagliati.
Secondo appello luglio 2010 Testo
della parte di logica con soluzioni e commenti dettagliati.
Argomenti corso - Programma definitivo:
PARTE 1 Semantic Tableaux per la logica proposizionale modale.
Martedi 6 Ottobre: Logica classica come logica della verita`.
Semantic tableaux per la logica proposizionale classica;
teorema di completezza.
Mercoledi 7 Ottobre: Semantica di Kripke della logica proposizionale
modale K.
Giovedi 8 Ottobre:NJ Teorema di completezza per la logica K.
Martedi 13 Ottobre: Semantica di Kripke per altre logiche modali
K4, S4.
Estensioni della procedura semantic tableaux.
Mercoledi 14 Ottobre continuazione.
Giovedi 15 Ottobre continuazione.
Prerequisiti Calcolo dei sequenti.
Martedi 20 Ottobre Calcolo dei predicati del primo ordine. Richiami di
semantica.
Mercoledi 21 Ottobre Procedura semantic taleaux per il calcolo dei
predicati del primo ordine.
Giovedi 22 Ottobre Teorema di completezza del calcolo dei predicati
del primo ordine.
Calcolo dei Sequenti Martedi 27 Ottobre Calcolo dei sequenti, proprieta` della sottoformula,
regola del taglio. Permutazione delle inferenze.
Eliminazione del taglio e normalizzazione delle prove. Normalizzazione forte
e debole.
Mercoledi 28 Ottobre Logica proposizionale moltiplicativa MLL-.
Teorema di eliminazione del taglio. Reti di prova, mappa dalle derivazioni
di sequenti alle reti di prova per la logica MLL-.
Giovedi 29 Ottobre Logica affine (MLL- + Weakening).
Coppie critiche. Molteplicita` di forme normali. Teorema di normalizzazione
debole. (cenni sulle reti di prove? )
Parte 3 Logica intuizionistica.
Martedi 3 Novembre Logica intuizionistica come logica della asseribilita`
e interpretazione di Heyting-Kolmogorov della logica intuizionistica.
Mercoledi 4 Novembre continuazione
Giovedi 5 Novembre Deduzione naturale intuizionista (frammento
implicativo con prodotti). Corrispondenza di Curry-Howard (cenni).
Martedi 10 Novembre
Corrispondenze fra deduzione naturale e calcolo dei sequenti.
Mercoledi 11 Novembre Interpretazioni modali della logica
intuizionistica (cenni)
Giovedi 12 Novembre Ancora sulla corrispondenza tra deduzione naturale
e calcolo dei sequenti.
Martedi 17 Novembre Ricapitolazione.
Giovedi 18 Novembre Logica temporale, tempo lineare.
Giovedi 19 Novembre Automi di Buchi
Lezione di recupero e ripasso
Venerdi 22 gennaio 2010 ore 10:30 Aula I
Lutz, Carsten. Temporal logic Logica temporale , in particolare pp.1-17.
Stirling, Colin. Models and calculi for concurrent computation,
modal and temporal logics. In Handbook of Modal Logic editors
P. Blackburn, J. van Benthem and F. Wolter.
Synsem.pdf,
Girard, J.-Y. : Linear Logic, its syntax and semantics, Advances
in Linear Logic, eds Girard, Lafont, Regnier, London Mathematical Society
Lecture Notes Series 222, Cambridge University Press 1995.
Coursework:
Compito per casa 1:pdf
Assegnato: 8 ottobre 2009 -- da consegnare: 15 ottobre. Soluzione Compito per casa 1:PDF
oppure
Lovato 1.
Si noti che in Es 1(e) tutti i sequenti hanno al massimo una formula
nel succedente.
In Es 2(b) un controesempio alla invertibilità semantica del Cut
moltiplicativo è dato da
Γ1 = bottom , Γ2 = top ∆1 = A , ∆2 = bottom,
dove bottom è una costante proposizionale contraddittoria
e top una costante proposizionale valida.
Compito per casa 2:pdf
Assegnato: 22 ottobre 2009 -- da consegnare: 29 ottobre. Soluzione Compito per casa 2:Lovato 2.
Si noti che in Es 2 nell'applicazione della procedura è
stato omesso il termine iniziale a nel sequente-conclusione.
Questo non ha conseguenze in questo caso: un tale termine non
comparirebbe nella formula atomica L(a1,a0) che consente
di chiudere il ramo considerato.
Compito per casa 3:pdf
Assegnato: 2 novembre 2009 -- da consegnare: 9 novembre. Soluzione Compito per casa 3:Lovato 3.
Compito per casa 4: pdf
Assignato: 12 novembre 2009 -- da consegnare: 19 novembre. Soluzione Compito per casa 4:Lovato 4.
Complementi su deduzione naturale, calcolo dei sequenti,
normalizzazione, eliminazione del cut pdf