Dettagli sull'Insegnamento per l'A.A. 2011/2012
Nome:
Metodi Formali / Formal Methods in Computer Science
Informazioni
Erogazione:
Laurea Magistrale in Informatica 1° anno curriculum Generale Obbligatorio
Lingua:
Inglese
Prerequisiti
Basic notions of mathematical logic and functional programming are helpful.
Obiettivi
Knowledge: basic notions of term rewriting systems and related properties,natural logic, intuitionistic logic and deduction process, definitions
and proofs in the Coq system.
Abilities: a student completing this course should be able to reason on properties of terms modulo an equational theory, define simple
notions in a proof assistant, such as Coq, and then prove inductive and non-inductive properties.
Expected behaviour: interest in the formal encoding of notions in a logic and in the formal derivation of properties.
Sillabo
- 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.
- Termini del prim'ordine, sostituzioni, sostituzioni istanziatrici ed unificatrici, mgu. Algoritmo di unificazione sintattica. Sistemi di riscrittura di termini. Terminazione: ordinamenti di riduzione, di semplificazione e per cammino ricorsivo (rpo).
- Confluenza: sovrapposizione di regole, coppie critiche, 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). E-unificazione di termini, relazione di narrowing, procedura di E-unificazione basata su narrowing, narrowing normale e basilare.
- Formule booleane, soddisfacibilità, tautologia. Formule in forma CNF ed algoritmo di Davis- Putnam. Deduzione naturale. Logica predicativa: predicati, funzioni, variabili, quantificatori, regole di deduzione naturale. Forma prenex DNF.
- Introduzione alle logiche di ordine superiore e al lambda-calcolo. Lambda-calcolo senza tipi, beta-riduzione, teoria dei tipi semplice, un calcolo per l'assegnamento di tipi, polimorfismo.
- Introduzione alla dimostrazione di teoremi nel proof-assistant HOL e definizione di tipi ricorsivi in HOL.
Testi di riferimento
- L. Thery, Note sul corso in italiano, solo la parte relativa alla Logica (credito 4 del sillabo) http://www-sop.inria.fr/marelle/Laurent.Thery/formal
- / J.-G. Smaus, Pearls of Computer-Supported Modeling and Reasoning - Lecture in l'Aquila Testo relativo al credito 5 del sillabo. http://www.informatik.uni-freiburg.de/~ki/teaching/ws0910/csmr/aquila.html
- 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. 1998. Testo relativo al credito 1 del sillabo. Copia disponibile presso copisteria interna e scansione pdf disponibile sul web http://www.di.univaq.it/monica/MFI/NoteARS.pdf
- Inverardi, M. Nesi e M. Venturini Zilli, Sistemi di Riscrittura per Termini del Prim'Ordine , Dipartimento di Matematica Pura e Applicata, Università degli Studi di L'Aquila. 1999. Testo relativo ai crediti 2 e 3 del sillabo. Copia disponibile presso copisteria interna e scansione pdf disponibile sul web http://www.di.univaq.it/monica/MFI/NoteSRT.pdf
Modalità d'esame
La prova di esame consiste in una prova scritta più una prova orale.
Aggiornamenti alla pagina del corso
Le informazioni sulle editioni passate di questo corso sono disponibili per i seguenti anni accademici:
Per leggere le informazioni correnti sul corso, se ancora erogato, consulta il catalogo corsi di ateneo.
Ultimo aggiornamento delle informazioni sul corso: 11 giugno 2012, 16:24