Course on Formal Methods / Modulo di Metodi Formali dell'Informatica
2010-11
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]
Boolean formulae, satisfiability, tautology. CNF and Davis-Putnam algorithm.
Natural deduction. 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]
Introduction to theorem proving in the HOL proof-assistant and recursive
type definition. [5]
[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.
Copia
disponibile in formato elettronico
e presso copisteria interna della Facoltà.
The English version of (a part of) the lecture
notes on Abstract Reduction Systems is available at the photocopy shop inside
the Faculty (near the main entrance of the building Coppito 1) and as an
electronic copy.
[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.
Copia
disponibile in formato elettronico e
presso copisteria interna della Facoltà.
The English version of (a part of) the lecture
notes on Term Rewriting Systems is available at the photocopy shop inside
the Faculty and as an electronic copy.
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.
Fino al paragrafo sulla forma Prenex DNF (escluso l'algoritmo di Stalmarck).
A preliminary
English version
of (part of) Prof. Théry's notes on logics is available.
This version is partial as some notes on predicate logic,
natural deduction and prenex DNF are still to be translated.
[4] J.-G. Smaus,
Pearls of Computer-Supported Modeling and Reasoning - Lecture in l'Aquila.
Slides 44-68 (file all_slides.pdf).
[5] M. Nesi,
A short note
on higher order logic and the HOL proof assistant.
An electronic version of the HOL basic rules of inference (modulo rotation of the document).
Ultimo aggiornamento: 24/03/2011.