Parte A: Teoria strutturale della dimostrazione: calcoli delle sequenze; eliminazione delle cesure, con applicazioni.
Parte B: Logiche modali dinamiche, temporali, epistemiche.
(2) Per approfondimenti:
[Parte A] A.S. Troelstra, H. Schwichtenberg, "Basic proof
theory", Cambridge University Press 1996.
[Parte B] P. Blackburn et al. (eds.), "Handbook of Modal Logic", Elsevier 2007.
Obiettivi Formativi
Il corso si propone di fornire agli studenti la conoscenza delle principali
problematiche e metodologie (i) della teoria stutturale della dimostrazione (relativamente alla logica classica e intuizionistica e ad alcune logiche sottostrutturali) e (ii) delle logiche modali con specifici operatori infinitari/di punto fisso (dinamiche, temporali, epistemiche).
Prerequisiti
Il corso propedeutico da 12 CFU di Logica (CdS triennale), o conoscenze
equivalenti (in questo caso parlare con il docente prima dell'iscrizione al corso).
Metodi Didattici
lezioni frontali (+ esercitazioni)
Altre Informazioni
.
Modalità di verifica apprendimento
esame orale
Programma del corso
Parte A. (i) calcoli delle sequenze (L-calcoli di Gentzen; calcoli di tipo G3)
per la logica classica elementare e per quella intuizionistica elementare; (ii)
eliminazione delle cesure ('Hauptsatz' di Gentzen); (iii) studio delle proprietà delle
dimostrazioni prive di cesure, con applicazioni (lemma di Maehara e interpolazione; teorema di Herbrand); (iv) logiche sottostrutturali (in particolare logica lineare affine e logica lineare).
(Parte B) (i)logica modale di base e semantica di Kripke; (ii) completezza: metodi del modello canonico e di filtrazione; (iii) logica proposizionale dinamica PDL e sue varianti; (iv) logiche temporali lineari (LTL) e ramificate (computational tree logic CTL); (v) logica della common knowledge.