Dettagli sull'Insegnamento per l'A.A. 2011/2012

Prerequisiti

Basic notions of mathematical logic and functional programming are helpful.

Obiettivi

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.

Sillabo

• Sistemi di riduzione astratti, forma normale, convertibilità, grafi di riduzione. Proprietà di confluenza e Church-Rosser e loro equivalenza. Locale confluenza, terminazione, canonicità. Principio di induzione noetheriana, lemma di Newman e sua dimostrazione.
• Termini del prim'ordine, sostituzioni, sostituzioni istanziatrici ed unificatrici, mgu. Algoritmo di unificazione sintattica. Sistemi di riscrittura di termini. Terminazione: ordinamenti di riduzione, di semplificazione e per cammino ricorsivo (rpo).
• Confluenza: sovrapposizione di regole, coppie critiche, Lemma di Huet e sua dimostrazione. Problema della parola e sua decidibilità, teorema di Knuth-Bendix. Procedure di completamento tramite regole di inferenza, terminazione e divergenza del completamento (pattern di divergenza). E-unificazione di termini, relazione di narrowing, procedura di E-unificazione basata su narrowing, narrowing normale e basilare.
• Formule booleane, soddisfacibilità, tautologia. Formule in forma CNF ed algoritmo di Davis- Putnam. Deduzione naturale. Logica predicativa: predicati, funzioni, variabili, quantificatori, regole di deduzione naturale. Forma prenex DNF.
• Introduzione alle logiche di ordine superiore e al lambda-calcolo. Lambda-calcolo senza tipi, beta-riduzione, teoria dei tipi semplice, un calcolo per l'assegnamento di tipi, polimorfismo.
• Introduzione alla dimostrazione di teoremi nel proof-assistant HOL e definizione di tipi ricorsivi in HOL.

Testi di riferimento

• 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   

Modalità d'esame

La prova di esame consiste in una prova scritta più una prova orale.

Risorse Internet

Aggiornamenti alla pagina del corso

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