Introduzione alla Logica di Ordine Superiore. Introduzione all'uso del sistema di dimostrazione interattiva HOL. Alcuni esempi di formalizzazione nel sistema HOL. Sviluppo di un progetto individuale di formalizzazione.
John Harrison, “Handbook of Practical Logic and Automated Reasoning” Cambridge University Press, 2009
John Harrison, HOL Light TutorialJohn Harrison, The HOL Light Manual
Obiettivi Formativi
Conoscenze: Conoscenze di base di Calcolo Simbolico Assistito dal Computer e di Verifica Automatica delle Dimostrazioni in Algebra e Geometria.
Competenze acquisite Conoscere il funzionamento di un sistema di dimostrazione interattivo.
Capacità acquisite al termine del corso: Saper verificare la dimostrazione di un semplice teorema di Algebra o diGeometria con l'aiuto di un sistema di dimostrazione interattivo (adesempio Coq, HOL, Isabelle).
Prerequisiti
Corsi raccomandati: Tutti i corsi dei settori disciplinari MAT/01 Logica Matematica, MAT/02 Algebra, Mat/03 Geometria, INF/01Informatica.
Metodi Didattici
Numero di ore totali del corso: 225
Numero di ore per studio personale e altre attività formative di tipo individuale: 162
Numero di ore relative alle attività in aula: 63
Altre Informazioni
Orario di ricevimento
Martedi’, 14.30-16.30
Modalità di verifica apprendimento
Prova Orale
Programma del corso
Introduzione alla Logica di Ordine Superiore: Lambda Calcolo e Teoria dei Tipi.Lambda Calcolo come fondamento della Programmazione Funzionale.Termini e tipi della Logica di Ordine Superiore.Regole di inferenza, assiomi, teoremi.Introduzione all'uso del sistema di dimostrazione interattiva HOL. Elementi di programmazione in ML. Conversioni e calcolo simbolico. Dimostrazione interattiva e tattiche elementari. Dimostrazione automatica, procedure di decisione per l'aritmetica, l'analisi reale e complessa, gli spazi vettoriali euclidei e la manipolazione simbolica de espressioni polinomiali e razionali.Alcuni esempi di formalizzazione nel sistema HOL: Esempi elementari di teoremi e teorie formalizzate in HOL. La libreria delle teorie sviluppate in HOL.Sviluppo di un progetto individuale di formalizzazione.