# Course Details for A.Y. 2011/2012

#### 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,natural logic, intuitionistic logic and deduction process, definitions
and proofs in the Coq system.
Abilities: a student completing this course should be able to reason on properties of terms modulo an equational theory, define simple
notions in a proof assistant, such as Coq, and then prove inductive and non-inductive properties.
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 in italiano, solo la parte relativa alla Logica (credito 4 del sillabo) 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. 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. Copia disponibile presso copisteria interna e scansione pdf disponibile sul web http://www.di.univaq.it/monica/MFI/NoteARS.pdf
* *
- 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. Copia disponibile presso copisteria interna e scansione pdf disponibile sul web 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: 11 giugno 2012, 16:24*