Course Details for A.Y. 2012/2013
Name:
Metodi Formali / Formal Methods in Computer Science
Basic information
Degree(s):
Laurea Magistrale in Informatica 1° anno curriculum Generale Obbligatorio
Language:
English
Course Objectives
Knowledge: basic notions of term rewriting systems and related properties, propositional logic, predicate calculus, natural deduction, proof and derivation.
Abilities: a student completing this course should be able to reason on properties of terms modulo an equational theory or using a given logic by applying deduction rules.
Expected behaviour: interest in the formal encoding of notions in a logic and in the formal derivation of properties.
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.
- Introduction to theorem proving in the HOL proof-assistant and recursive type definition.
Prerequisites and Learning Activities
Basic notions of mathematical logic and functional programming are helpful.
Assessment Methods and Criteria
Written and oral examination
Textbooks
- L. Thery, Note sul corso Note relative al credito 4 del sillabo (in italiano, solo la parte relativa alla Logica) http://www-sop.inria.fr/marelle/Laurent.Thery/formal
- / J.-G. Smaus, Pearls of Computer-Supported Modeling and Reasoning - Lecture in l'Aquila Testo relativo al credito 5 del sillabo (disponibile solo in inglese). 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. Testo relativo al credito 1 del sillabo. Versione elettronica in formato pdf disponibile sul web (versione ridotta disponibile anche in inglese). 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. Testo relativo ai crediti 2 e 3 del sillabo. Versione elettronica in formato pdf disponibile sul web (versione ridotta disponibile anche in inglese). http://www.di.univaq.it/monica/MFI/NoteSRT.pdf
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: 08 ottobre 2012, 10:28