Questo sito utilizza solo cookie tecnici, propri e di terze parti: continuando la navigazione ne accetti l'uso. Acconsento Vorrei maggiori informazioni
Naviga nel sito del Dipartimento:
Naviga nel sito della Didattica:

Programme of Course "Formal Methods"

Code:

DT0202

Type of course unit:

Level of course unit:

Semestre:

2° semestre

Number of credits:

Laurea Magistrale in Informatica: 6 (workload 150 hours)

Teachers:

Monica Nesi (monicadotnesiatunivaqdotit)

1. Course Objectives

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.

2. Course Contents and learning outcomes (Dublin Descriptors)

Topics of the course include:

  • 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.

On successful completion of this course, the student should

  • 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.

3. Course Prerequisites

Basic notions of mathematical logic and functional programming are helpful.

4. Teaching methods and language

Lectures and exercises

Language:Inglese[info]

Reference textbooks

  • L. Thery, Lectures notes.
  • J.-G. Smaus, Pearls of Computer-Supported Modeling and Reasoning - Lecture in l'Aquila.
  • 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.
  • 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.

5. Assessment Methods

La prova di esame consiste in una prova scritta più una prova orale.

Course information last updated on: 20 aprile 2016, 10:29