This site uses only proprietary and third party technical cookies. By continuing to browse the site you are agreeing to our use of cookies. I agree I want to find out more
Browse the Department site:
Browse the Teaching site:

Programme of Course "Formal Methods"



Type of course unit:

Level of course unit:


2nd semester

Number of credits:

Master Degree in Computer Science: 6 (workload 150 hours)


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:

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

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


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

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

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