Dettagli sull'Insegnamento per l'A.A. 2014/2015

Sillabo

• Sistemi di riduzione astratti, forma normale, convertibilità, confluenza e Church-Rosser e loro equivalenza. Locale confluenza, terminazione, canonicità. Principio di induzione noetheriana, lemma di N
• Sistemi di riscrittura di termini. Terminazione: ordinamenti di riduzione, di semplificazione e per cammino ricorsivo (rpo), ordinamento su multinsiemi. Confluenza: sovrapposizione di regole, coppie c
• E-unificazione di termini, relazione di narrowing, procedura di E-unificazione basata su narrowing, narrowing normale e basilare. [2]
• Formule booleane, soddisfacibilita', tautologia. Formule in forma CNF ed algoritmo di Davis-Putnam. Refutazione ed algoritmo di Stalmarck. Deduzione naturale: logica intuizionistica e logica naturale
• Logica predicativa: predicati, funzioni, variabili, quantificatori, regole di deduzione naturale. Forma prenex DNF ed algoritmo di Presburger
• Isomorfismo di Curry-Howard: equivalenza tra tipo e formula e tra programma e prova. Introduzione al sistema Coq: tipi, proposizioni, insiemi, tipi dipendenti. Definizioni induttive e non induttive. F

Testi di riferimento

• M. Nesi e M. Venturini Zilli, Sistemi di riduzione astratti' , Research Report SI-98/06, Facolta' di Scienze MM.FF.NN., Universita' degli Studi di Roma ``La Sapi. 1998.. Copia disponibile presso copisteria interna.    
• P. Inverardi, M. Nesi e M. Venturini Zilli,, Sistemi di Riscrittura per Termini del Prim'Ordine' , Dipartimento di Matematica Pura e Applicata, Universita' degli Studi di L'Aquila. 1999.. Copia disponibile presso copisteria interna e all'indirizzo http://www.di.univaq.it/monica/    

Modalità d'esame

La prova di esame consiste in una prova scritta sulle due parti del corso + una prova orale sulle due parti del corso + un'attivita' progettuale per la parte di laboratorio correlata agli argomenti del corso da concordare con il docente.

Risorse Internet

Aggiornamenti alla pagina del corso

• A.A. 2013/2014
• A.A. 2014/2015
• A.A. 2015/2016
• A.A. 2016/2017
• A.A. 2017/2018
• A.A. 2018/2019
• A.A. 2019/2020