Course Details for A.Y. 2017/2018
Name:
Metodi Formali dell'Informatica + Laboratorio /
Basic information
Credits:
: Master Degree in Computer Science 12 CFU (b)
Degree(s):
Master Degree in Computer Science 2nd anno curriculum General
Language:
Italian
Course Content
- 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
Assessment Methods and Criteria
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.
Textbooks
- 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/
Course page updates
This course page is available (with possible updates) also for the following academic years:
To read the current information on this course, if it is still available, go to the university course catalogue .
Course information last updated on: 21 febbraio 2008, 11:35