Course Details for A.Y. 2012/2013

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   

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