Course Details for A.Y. 2010/2011
Name:
Metodi Formali dell'Informatica / Formal Methods in Computer Science
Basic information
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). [1] Signature, first-order terms, positions, substitutions.Equational theory E and equational deduction.
- Term rewriting systems. Termination: reduction ordering, simplification ordering, recursive path ordering, multiset 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. [2]
- Boolean formulae, satisfiability, tautology. Formulae in CNF and Davis-Putnam's algorithm. Refutation and Stalmarck's algorithm. Natural deduction: intuitionistic logic and natural logic.
- Predicate logic: predicates, functions, variables, quantifiers,rules of natural deduction. Prenex form DNF and Presburger's
- Curry-Howard's Isomorphism: equivalence between types and formulae and between programs and proofs. Introduction to the Coq system: types, propositions, sets, dependent types. Inductive definitions and non-inductive definitions. Recursive functions and non-recursive functions. Proofs in Coq: proofs by recursion and by case analysis. Interactive proofs and basic tactics. [3]
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 1 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 ai crediti 2 e 3 del sillabo. Copia disponibile presso copisteria interna. 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 4 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 5 e 6 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: 23 febbraio 2011, 18:45