Metodi matematici per l'informatica (2012/2013)

Codice insegnamento
4S02855
Crediti
6
Coordinatore
Ugo Solitro
Settore disciplinare
INF/01 - INFORMATICA
Lingua di erogazione
Italiano
Pagina Web
http://profs.sci.univr.it/~solitro/beta/XMeth/index.html
L'insegnamento è organizzato come segue:
Attività Crediti Periodo Docenti Orario
Parte 1 3 I semestre Ugo Solitro
Parte 2 3 I semestre Gianluigi Bellin

Orario lezioni

I semestre
Attività Giorno Ora Tipo Luogo Note
Parte 1 martedì 13.30 - 15.30 lezione Aula M  
Parte 1 venerdì 13.30 - 15.30 lezione Aula M  

Obiettivi formativi

Un'introduzione alla teoria della computabilità generale e alla logica computazionale.

Programma

Modulo: Computabilità.
-------
Introduzione.
Automi, Linguaggi e Grammatiche. Risultati prinicipali.

Calcolabilità
Algoritmi. Sistemi di Calcolo Effettivo: Macchine di Turing, Funzioni parziali ricorsive, ...
Risultati fondamentali. Tesi di Church. Aritmetizzazione e Universalità. Problemi insolubili.
Teoria matematica della Ricorsione.

Complessità.
Classi di Complessità. NP-Completezza.
Complementi
------------------------

Modulo: Logica computazionale.

Rappresentazione di prove ed algoritmi.
Calcoli dei sequenti, eliminazione del taglio, semantic tableaux. Deduzione naturale intuizionistica.

Lambda calcolo, proprietà di Church-Rosser. Rappresentabilità delle funzioni parziali ricorsive. Tipi semplici e tipabilità.

Corrispondenza di Curry Howard e teorema di normalizzazione debole del lambda calcolo con tipi semplici. Complementi.

Modalità d'esame

L'esame prevede una prova di verifica per ciascun modulo e un colloquio orale finale.

Testi di riferimento
Attività Autore Titolo Casa editrice Anno ISBN Note
Parte 1 John E. Hopcroft, Rajeev Motwani, Jeffrey D. Ullman Introduction to Automata Theory, Languages and Computation (Edizione 2) Addison-Wesley 2000 0201441241 testo di riferimento