Dettagli sull'Insegnamento per l'A.A. 2014/2015
Nome:
Metodi Formali / Formal Methods
Informazioni
Crediti:
: Master Degree in Computer Science 6 CFU (b)
Erogazione:
Master Degree in Computer Science 1st anno curriculum GSEEM Compulsory
Master Degree in Computer Science 1st anno curriculum General Compulsory
Lingua:
Inglese
Prerequisiti
Basic notions of mathematical logic and functional programming are helpful.
Obiettivi
The goal of this course is to introduce symbolic techniques for the specification and verification of systems properties based on equational reasoning and theorem proving. On successful completion of this course, the student should understand the basic notions of first-order rewriting and logic, and be able to reason on properties of terms by means of symbolic manipulation modulo an equational theory or the deduction rules of a given logic.
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.
Descrittori di Dublino
Alla fine del corso, lo studente dovrebbe
- have profound knowledge of the basic concepts of first-order rewriting and first-order logic, relate the termination and confluence properties, have knowledge and understanding of pattern matching, syntactic and semantic unification, have knowledge and understanding of the natural deduction rules for propositional logic and predicate calculus, understand lambda-calculus as the base of the syntax for higher-order logic and functional programming;
- understand and apply definitions, inference rules and theorems;
- analyse and discuss different variants of a concept, discuss different proof techniques for deriving properties of terms and formulae;
- explain and illustrate the fundamental notions of unification of terms, reduction ordering and critical pairs, explain the word problem and the completion of equational theories;
- demonstrate skill in equational reasoning, formal derivation and symbolic manipulation, demonstrate ability to derive types for higher-order terms and properties of terms and formulae, demonstrate capacity for building proofs.
Testi di riferimento
- L. Thery, Lectures notes Credit 4 of syllabus (In Italian and English, only the part related to Logic). http://www-sop.inria.fr/marelle/Laurent.Thery/formal
- / J.-G. Smaus, Pearls of Computer-Supported Modeling and Reasoning - Lecture in l'Aquila Credit 5 of syllabus (Available only in English). 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. Credit 1 of syllabus. Electronic version in pdf format available on the web (reduced version available also in English). http://www.di.univaq.it/monica/MFI/NoteARS.pdf
- P. 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. Credits 2-3 of syllabus. Electronic version in pdf format available on the web (reduced version available also in English). 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 luglio 2014, 01:04