Il corso introduce sistemi logici fondamentali per le applicazioni all'informatica e per la rappresentazione astratta dei processi computazionali in modo rigoroso ma radicato nella pratica .
Il corso presenta i sistemi di Gentzen, calcolo dei sequenti e deduzione naturale; la procedura semantic tableaux per la dimostrazione dei teoremi di consistenza e completezza per la semantica di Kripke delle logiche modali K, K4, S4 e per la logica intuizionistica, via la traduzione in S4; la corrispondenza di Curry-Howard tra lambda calcolo tipato semplice e deduzione naturale intuizionistica; proprieta` di Church-Rosser e teoremi di normalizzazione forte; categorie cartesiane chiuse e semantiche categoriali della logica intuizionistica.
Esame scritto o orale
******** CSS e script comuni siti DOL - frase 9957 ********p>