Dimostrazione interattiva applicata alla geometria e all'algebra. Introduzione alla Logica di Ordine Superiore. Introduzione all'uso del sistema di dimostrazione interattiva HOL. Procedure di decisione in Geometria e in Algebra. Alcuni esempi di formalizzazione nel sistema HOL in algebra e geometria.
John Harrison, "Handbook of Practical Logic and Automated Reasoning" Cambridge University Press, 2009
John Harrison, HOL Light Tutorial (liberamente disponibile online)
John Harrison, The HOL Light Manual (liberamente disponibile online)
Robert M. Solovay, R. D. Arthan, John Harrison, "Some new results on decidability for elementary algebra and geometry" (arXiv 2009)
Obiettivi Formativi
Il Corso ha l’obiettivo di fornire agli studenti conoscenze e capacità di comprensione basilari riguardo alla Formalizzazione della Matematica, al Calcolo Simbolico e alle procedure di decisione in Algebra e in Geometria. Il corso intende anche sviluppare le capacità tecniche di base e le capacità critiche necessarie per applicare le conoscenze acquisite alla modellizzazione e risoluzione di problemi matematici in vari ambiti. Particolare attenzione viene posta a sviluppare negli studenti le abilità comunicative necessarie per il lavoro di gruppo. Il corso copre argomenti e fornisce capacità di apprendimento importanti per gli ambiti della Matematica Formale e dei Fondamenti Matematici dell'Informatica e del Calcolo Scientifico.
Prerequisiti
Nessuno
Metodi Didattici
Lezioni (in diretta o registrate): esposizione critica della teoria in programma, con interazione diretta docente-studente (se in diretta) o con colloqui successivi (se registrate) per facilitare e assicurare la piena comprensione della materia.
Esercitazioni: guida per gli studenti alla modellizzazione e risoluzione di una vasta scelta di problemi variegati riguardanti la Dimostrazione al Computer, il Calcolo Simbolico, la Formalizzazione della Matematica e le procedure di decisione in Algebra e in Geometria. Le esercitazioni sono condotte in modo da:
-- aiutare gli studenti a sviluppare le capacità di applicare e comunicare le conoscenze acquisite;
-- migliorare la loro indipendenza di giudizio;
Le esercitazioni sono basate su sessioni pratiche con un software di dimostrazione e calcolo simbolico.
Classe virtuale: sviluppo dell’interazione online docente-studente, diffusione di dispense integrative, di raccolte di esercizi e di esempi di testi di prove d’esame.
Nota: I testi e le dispense proposti o consigliati contengono materiale supplementare per approfondimento personale e per ulteriore studio.
Altre Informazioni
Nessuna.
Modalità di verifica apprendimento
L'esame prevede due fasi:
1. Preparazione di un progetto individuale (in genere una formalizzazione al computer nel dimostratore di teoremi HOL Light) accompagnato da una breve relazione scritta.
2. Discussione orale del progetto.
Il candidato deve inviare all'insegnante la relazione e il codice prima dell'esame orale.
Il progetto è concepito per valutare la capacità dello studente di applicare le tecniche illustrate nel corso. Particolare attenzione è rivolta alla correttezza, l'originalità e l'efficacia della soluzione proposta.
L'esame orale valuterà il grado di comprensione della teoria presentata nel corso. La valutazione prenderà in considerazione anche le capacità comunicative (incluso l'uso appropriato della terminologia e del linguaggio matematico) e l'atteggiamento di pensiero critico del candidato.
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. Procedure di decisione per l'aritmetica lineare, per il calcolo polinomiale e le sue applicazioni in geometria. Alcuni esempi di formalizzazione nel sistema HOL. La libreria delle teorie sviluppate in HOL sull'analisi multivariata, l'algebra e l'analisi dei numeri reali e complessi e dei quaternioni.