Logica computazionale (2007/2008)

Corso a esaurimento

Codice insegnamento
4S01115
Docente
Gianluigi Bellin
crediti
5
Settore disciplinare
MAT/01 - LOGICA MATEMATICA
Lingua di erogazione
Italiano
Periodo
1° Q dal 3-ott-2007 al 4-dic-2007.
Pagina Web
http://profs.sci.univr.it/~bellin

Orario lezioni

1° Q
Giorno Ora Tipo Luogo Note
martedì 14.30 - 16.30 lezione Aula B  
mercoledì 12.30 - 13.30 lezione Aula C  
venerdì 9.30 - 11.30 lezione Aula A  
venerdì 14.30 - 16.30 lezione Aula L  

Obiettivi formativi

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 .

Programma

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.

Modalità d'esame

Esame scritto o orale

Materiale didattico

Documenti