Course Details for A.Y. 2014/2015

The information on this page refer to the academic year 2014/2015. Therefore, several links are not available and data may be incomplete. To read the current information on the course, if it is still available, go to the university course catalogue . To read information relating other academic years, use the list at the bottom of this page.

A. Year:

2014/2015

Name:

Metodi Formali / Formal Methods

Type:

Course

Basic information

Code:

F0191

Sector:

INF/01

Credits:

: Master Degree in Computer Science 6 CFU (b)

Term:

1^st semester

Degree(s):

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

Language:

English

Teacher(s):

Monica Nesi

Same as:

Metodi Formali dell'Informatica

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.

Course Content

Abstract reduction systems, normal form, convertibility. Confluence, Church-Rosser property and their equivalence. Local confluence, termination, canonicity. Principle of Noetherian Induction and Newman's lemma (proof included).
First-order terms, substitutions, match and mgu. Algorithm of syntactic unification. Equational theories and equational deduction. Term rewriting systems. Termination: reduction ordering, simplification ordering, recursive path ordering.
Confluence: overlapping of rewrite rules, critical pairs, Huet's lemma (proof included). The word problem, completion procedures, divergence of completion. E-unification of terms, narrowing relation, E-unification procedure based on normalized and basic narrowing.
Boolean formulae, satisfiability, tautology. Formulae in CNF and Davis-Putnam's algorithm. Natural deduction. Predicate logic: predicates, functions, variables, quantifiers,rules of natural deduction. Prenex DNF.
Introduction to higher-order logics and lambda-calculus. Untyped lambda-calculus, beta-reduction, simple type theory, type assignment calculus, polymorphism.

Learning Outcomes (Dublin Descriptors)

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.

Prerequisites and Learning Activities

Basic notions of mathematical logic and functional programming are helpful.

Assessment Methods and Criteria

Written and oral examination. The written exam can be split into a midterm exam + a final exam at the end of the course.

Textbooks

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

Internet Resources

Homepage:

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

Course page updates

This course page is available (with possible updates) also for the following academic years:

To read the current information on this course, if it is still available, go to the university course catalogue .

Course information last updated on: 11 luglio 2014, 01:04