Laurea in Informatica


Corso di Metodi Formali dell'Informatica
(a.a. 2001-02)


Riscrittura (Docente: Monica Nesi)

Sistemi di riduzione astratti, forma normale, convertibilità, grafi di riduzione. Proprietà di confluenza e Church-Rosser e loro equivalenza. Locale confluenza, terminazione, canonicità. Principio di induzione noetheriana, lemma di Newman e sua dimostrazione [1].
Segnature, termini del prim'ordine, rappresentazione ad albero dei termini. Posizioni, occorrenze, sottotermini e contesti. Sostituzioni, sostituzioni istanziatrici ed unificatrici, mgu.
Identità ed equazioni, teoria equazionale E, relazione di riduzione in E, chiusura rispetto a sostituzioni ed operazioni. Deduzione equazionale, sistema deduttivo per l'uguaglianza modulo E. Modelli, validità, soddisfacibilità, varietà e teorema di completezza di Birkhoff.
Sistemi di riscrittura di termini, redesso, passo di riscrittura. Terminazione: ordinamenti di riduzione, di semplificazione e per cammino ricorsivo (rpo), ordinamento su multinsiemi. Confluenza: decidibilità della convertibilità, spectra delle regole, sovrapposizione di regole, coppie critiche, sistemi ambigui. Lemma di Huet e sua dimostrazione. Problema della parola e sua decidibilità, teorema di Knuth-Bendix. Procedure di completamento tramite regole di inferenza, terminazione e divergenza del completamento (pattern di divergenza).
Riscrittura modulo equazioni, E-unificazione di termini, insieme minimale e completo di E-unificatrici. Relazione di narrowing, procedura di E-unificazione basata su narrowing, narrowing normale e basilare, albero di derivazione di narrowing [2].

Logica e Prova (Docente: Laurent Théry)

Formule booleane, soddisfacibilità, tautologia. Formule in forma CNF ed algoritmo di Davis-Putnam. Refutazione ed algoritmo di Stålmarck. 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. Funzioni ricorsive e non ricorsive. Prove in Coq: prove per ricorsione e per casi. Prove interattive e tattiche di base [3].


Riferimenti bibliografici

[1] M. Nesi e M. Venturini Zilli, Sistemi di riduzione astratti, Research Report SI-98/06, Facoltà di Scienze MM.FF.NN., Università degli Studi di Roma "La Sapienza", March 1998. Copia disponibile presso copisteria interna.
[2] P. Inverardi, M. Nesi e M. Venturini Zilli, Sistemi di Riscrittura per Termini del Prim'Ordine, Rapporto Tecnico No.35, Dipartimento di Matematica Pura e Applicata, Università degli Studi di L'Aquila, Luglio 1999. Copia disponibile anche presso copisteria interna.
[3] L. Théry, Note sul corso di Metodi Formali dell'Informatica.