Dettagli sull'Insegnamento per l'A.A. 2014/2015

Le informazioni che state leggendo si riferiscono all'anno accademico 2014/2015. Per questo molti collegamenti non sono disponibili e i dati potrebbero essere incompleti. Per leggere le informazioni correnti sul corso, se ancora erogato, consulta il catalogo corsi di ateneo. Per consultare le informazioni relative ad altri anni accademici, usa la lista in fondo a questa pagina.

A. Accademico:

2014/2015

Nome:

Metodi Formali / Formal Methods

Tipo:

Corso singolo

Informazioni

Codice:

F0191

SSD:

INF/01

Crediti:

: Master Degree in Computer Science 6 CFU (b)

Periodo:

1^st semester

Erogazione:

Master Degree in Computer Science 1^st anno curriculum GSEEM Compulsory
Master Degree in Computer Science 1^st anno curriculum General Compulsory

Lingua:

Inglese

Docenti:

Monica Nesi

Mutua:

Metodi Formali dell'Informatica

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.

Risorse Internet

Homepage:

http://www.di.univaq.it/monica/didattica11-12.html

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