Module of Formal Methods
Lecturer: Monica Nesi
Abstract reduction systems, normal form, convertibility, reduction graphs.
Confluence property, Church-Rosser property and their equivalence.
Local confluence, termination, canonicity. Principle of noetherian induction,
Newman Lemma and its proof. [1]
First-order terms, substitutions, matching substitutions, unifiers, mgu.
Algorithm of syntactic unification. Term rewriting systems. Termination:
reduction ordering, simplification ordering, recursive path ordering.
[2]
Confluence: rules overlapping, critical pairs, Huet Lemma (with proof).
The word problem and its decidability, Knuth-Bendix Theorem.
Completion procedures through inference rules, termination and divergence of
completion (divergence pattern). E-unification of terms, narrowing relation,
E-unification procedure based on narrowing, normal and basic narrowing.
[2]
Propositional logic: boolean formulae, satisfiability, tautology, CNF and
Davis-Putnam algorithm.
Natural deduction for propositional logic.
Predicate logic: predicates, functions, variables,
quantifiers, rules of natural deduction. Prenex DNF.
[3]
Introduction to higher-order logics and lambda-calculus.
Untyped lambda-calculus, beta-reduction, simple type theory, type assignment
calculus, polymorphism. [4]
[1] 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", March 1998
(Italian version and
English (short) version,
where only those sections that are presented in the course have been
translated).
[2] P. Inverardi, M. Nesi e M. Venturini Zilli,
Sistemi di Riscrittura per Termini del Prim'Ordine,
Rapporto Tecnico No.35, Dipartimento di Matematica Pura e Applicata,
Università degli Studi di L'Aquila, Luglio 1999
(Italian version,
English (short) version).
Note that some notes and exercises on the rewriting part are available
(in Italian) in the Formal Methods section at the page of the
academic year 2008-09,
integrating the lecture notes [2],
as the teaching of the course was interrupted due to the earthquake.
[3] L. Théry,
Note sul corso di Metodi Formali dell'Informatica (up to prenex DNF,
Stalmarck algorithm excluded).
A preliminary
English version
of Prof. Théry's notes on logics is now available.
[4] J.-G. Smaus,
Pearls of Computer-Supported Modeling and Reasoning - Lecture in l'Aquila.
Slides 44-68 (file all_slides.pdf).