Course Details for A.Y. 2017/2018

The information on this page refer to the academic year 2017/2018. Therefore, several links are not available and data may be incomplete. To read the current information on the course, if it is still available, go to the university course catalogue . To read information relating other academic years, use the list at the bottom of this page.

A. Year:

2017/2018

Name:

Metodi Formali dell'Informatica + Laboratorio /

Type:

Course

Basic information

Code:

F2I014

Sector:

INF/01

Credits:

: Master Degree in Computer Science 12 CFU (b)

Term:

Degree(s):

Master Degree in Computer Science 2^nd anno curriculum General

Language:

Italian

Teacher(s):

Monica Nesi
Laurent Thery

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/

Internet Resources

Homepage:

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