Insegnamento mutuato da: B012995 - GEOMETRIA COMPUTAZIONALE SIMBOLICA Laurea Magistrale in MATEMATICA Curriculum APPLICATIVO
Lingua Insegnamento
Italiano.
Contenuto del corso
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 teorica e del calcolo scientifico.
Prerequisiti
Nessuno
Metodi Didattici
Lezioni frontali: esposizione critica della teoria in programma, con interazione diretta docente-studente 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;
Esercitazioni nel laboratorio informatico: sessioni pratiche con un software di dimostrazione e calcolo simbolico.
Piattaforma Moodle: 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.
Modalità di verifica apprendimento
Prova finale orale: Viene proposta una scelta di esercizi concepiti per valutare la capacità degli studenti di applicare le conoscenze teoriche e tecniche da loro acquisite alla modellizzazione e alla soluzione di problemi. Vengono valutate con particolare attenzione sia la correttezza dei procedimenti seguiti, sia l'originalità dei metodi adottati e la loro efficacia.
Vengono poste alcune domande sugli esercizi proposti per verificare la conoscenza e il grado di comprensione della teoria svolta nel corso. Vengono valutate con particolare attenzione sia la capacità di comunicare la materia in modo critico, sia l’uso di un linguaggio matematico appropriato.
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.