Logica applicata e dimostrazione interattiva.
Introduzione alla Logica di Ordine Superiore.
Introduzione all'uso del sistema di dimostrazione interattiva HOL.
Esempi di formalizzazione nel sistema HOL.
John Harrison, "Handbook of Practical Logic and Automated Reasoning" Cambridge University Press, 2009
John Harrison, HOL Light Tutorial
John 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 di Geometria con l'aiuto di un sistema di dimostrazione interattivo (adesempio Coq, HOL, Isabelle).
Prerequisiti
Nessuno
Metodi Didattici
Lezioni frontali, esercitazioni.
Altre Informazioni
Nessuna
Modalità di verifica apprendimento
Prova finale scritta e 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.