Course Details for A.Y. 2010/2011

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   

Internet Resources

Course page updates

• A.Y. 2010/2011
• A.Y. 2011/2012
• A.Y. 2012/2013
• A.Y. 2013/2014
• A.Y. 2014/2015
• A.Y. 2015/2016
• A.Y. 2016/2017
• A.Y. 2017/2018
• A.Y. 2018/2019
• A.Y. 2019/2020