ID:
SCV0314
Durata (ore):
48
CFU:
6
SSD:
LOGICA MATEMATICA
Sede:
Como - Università degli Studi dell'Insubria
Anno:
2024
Dati Generali
Periodo di attività
Secondo Semestre (17/02/2025 - 30/05/2025)
Syllabus
Obiettivi Formativi
Il corso si propone di fornire le conoscenze dei meccanismi di base dell'inferenza logica, attraverso lo studio delle fondamentali nozioni di logica proposizionale classica e del primo ordine. Tali conoscenze sono rivolte a formare e ad aumentare la capacità di astrazione delle informazioni attraverso la rappresentazione simbolica e quindi la capacità della comprensione di un linguaggio scientifico astratto. Verranno accennati alcuni approfondimenti su strumenti di carattere più applicativo come la correttezza dei programmi e la programmazione funzionale.
I risultati di apprendimento attesi comprendono la capacità di saper individuare eventuali errori in una argomentazione matematica, e di avere una proprietà di linguaggio tale da poter enunciare un teorema e descrivere una sua dimostrazione. Nello specifico, al termine del corso ci si attende lo studente abbia acquisito le seguenti abilità:
1. effettuare semplici dimostrazioni matematiche in un sistema formale tra quelli presentati.
2. effettuare dimostrazioni sulle proprietà di un sistema formale tra quelli presentati.
3. relazionare dimostrazioni e computazioni.
La conoscenza dei meccanismi logici del ragionamento matematico permette l’acquisizione di adeguate capacità per l'approfondimento delle proprie conoscenze e per lo sviluppo individuale di nuove competenze.
I risultati di apprendimento attesi comprendono la capacità di saper individuare eventuali errori in una argomentazione matematica, e di avere una proprietà di linguaggio tale da poter enunciare un teorema e descrivere una sua dimostrazione. Nello specifico, al termine del corso ci si attende lo studente abbia acquisito le seguenti abilità:
1. effettuare semplici dimostrazioni matematiche in un sistema formale tra quelli presentati.
2. effettuare dimostrazioni sulle proprietà di un sistema formale tra quelli presentati.
3. relazionare dimostrazioni e computazioni.
La conoscenza dei meccanismi logici del ragionamento matematico permette l’acquisizione di adeguate capacità per l'approfondimento delle proprie conoscenze e per lo sviluppo individuale di nuove competenze.
Prerequisiti
Per un proficuo apprendimento di questo insegnamento lo studente deve padroneggiare le nozioni matematiche e le tecniche dimostrative impartite nell’insegnamento fondamentale di Algebra e Geometria del primo anno, che dunque costituisce propedeuticità obbligatoria.
Metodi didattici
Lezione frontale in lingua italiana con l’ausilio di slides e approfondimenti alla lavagna.
Verifica Apprendimento
L’obiettivo della prova d’esame è l'accertamento dell’acquisizione delle conoscenze e delle abilità descritte nella sezione “Obiettivi Formativi”, valutando il livello di conoscenza e la capacità di applicare le nozioni e le tecniche dimostrative viste a lezione.
L’esame consiste in una prova scritta della durata di 90 minuti articolata secondo il seguente schema: (parte A) una/due domande aperte relative alla presentazione e applicazione delle nozioni presentate nell’insegnamento (enunciare teoremi o definizione, discussione dei concetti, specializzare un concetto ad un dominio specifico); (parte B) dimostrazione di uno dei teoremi presentati a lezione; (parte C) uno/due esercizi sullo schema di quelli presentati a lezione.
L’esame consiste in una prova scritta della durata di 90 minuti articolata secondo il seguente schema: (parte A) una/due domande aperte relative alla presentazione e applicazione delle nozioni presentate nell’insegnamento (enunciare teoremi o definizione, discussione dei concetti, specializzare un concetto ad un dominio specifico); (parte B) dimostrazione di uno dei teoremi presentati a lezione; (parte C) uno/due esercizi sullo schema di quelli presentati a lezione.
Contenuti
A. Introduzione
A1. aspetti burocratici e amministrativi, storia della logica, relazione con l’informatica (2 ore)
B. Logica Proposizionale
B1. concetto di induzione strutturale, sintassi, deduzione naturale (2 ore)
B2. esempi di dimostrazione formale (2 ore)
B3. semantica a tavole di verità, insiemi minimali di connettivi, forme normali disgiuntive e congiuntive, soddisfacibilità (4 ore)
B4. algebre di Boole (2 ore)
B5. teorema di correttezza, schema della dimostrazione e correttezza di semplici programmi (2 ore)
B6. completezza (2 ore)
C. Logica al Primo Ordine
C1. Sintassi, sostituzione, calcolo naturale (2 ore)
C2. esempi di deduzione, esempi di formalizzazione (2 ore)
C3. semantica alla Tarski, teorema di correttezza (2 ore)
C4. Risoluzione, unificazione, programmazione logica mediante esempi (4 ore)
D. Teoria dei Tipi Semplici
D1. λ-calcolo, sintassi, riduzioni (2 ore)
D2. esempi: tipi di dati in λ-calcolo, esempi: programmazione funzionale (4 ore)
D3. teoria dei tipi semplici, sintassi, riduzioni (2 ore)
D4. logica proposizionale intuizionista, sintassi, potenza espressiva (2 ore)
D5. isomorfismo Curry-Howard, dimostrazioni come programmi, correttezza per costruzione, normalizzazione forte, terminazione di programmi (2 ore)
E. Risultati limitativi
E1. teorema di compattezza, esempi di modelli non standard (2 ore)
E2. aritmetica di Peano, codifica (2 ore)
E3. lemma di punto fisso, teorema di incompletezza di Gödel (2 ore)
E4. funzioni calcolabili, tesi di Church-Turing, teorema di Cantor, esistenza di funzioni incalcolabili (2 ore)
E5. incalcolabilità e incompletezza, esempi: minori di grafi (2 ore)
Rispetto agli obiettivi formativi,
- la parte A1 è specificatamente diretta a formare il necessario linguaggio scientifico per affrontare il corso; tale linguaggio verrà approfondito in tutte le parte successive;
- le parti B1, B3, B5, C1, C3, D4, D5, E2 ed E3 sono principalmente dirette a formare le conoscenze relative all’inferenza logica, con le parti B2 e C2 specificatamente destinate a formare l’abilità di effettuare prove formali;
- le parti B4, B5, B6, C3, D1, D3, D5, E1, E2, E3 ed E5 sono dirette a formare le competenze relative alla capacità di astrazione formale, con qualche sovrapposizione con l’obiettivo precedente ove esso sia funzionale a raccordare le abilità;
- le parti B3, B5, C4, D2, D5 ed E4 sono destinate a consolidare gli obiettivi formativi precedenti in ambito informatico.
A1. aspetti burocratici e amministrativi, storia della logica, relazione con l’informatica (2 ore)
B. Logica Proposizionale
B1. concetto di induzione strutturale, sintassi, deduzione naturale (2 ore)
B2. esempi di dimostrazione formale (2 ore)
B3. semantica a tavole di verità, insiemi minimali di connettivi, forme normali disgiuntive e congiuntive, soddisfacibilità (4 ore)
B4. algebre di Boole (2 ore)
B5. teorema di correttezza, schema della dimostrazione e correttezza di semplici programmi (2 ore)
B6. completezza (2 ore)
C. Logica al Primo Ordine
C1. Sintassi, sostituzione, calcolo naturale (2 ore)
C2. esempi di deduzione, esempi di formalizzazione (2 ore)
C3. semantica alla Tarski, teorema di correttezza (2 ore)
C4. Risoluzione, unificazione, programmazione logica mediante esempi (4 ore)
D. Teoria dei Tipi Semplici
D1. λ-calcolo, sintassi, riduzioni (2 ore)
D2. esempi: tipi di dati in λ-calcolo, esempi: programmazione funzionale (4 ore)
D3. teoria dei tipi semplici, sintassi, riduzioni (2 ore)
D4. logica proposizionale intuizionista, sintassi, potenza espressiva (2 ore)
D5. isomorfismo Curry-Howard, dimostrazioni come programmi, correttezza per costruzione, normalizzazione forte, terminazione di programmi (2 ore)
E. Risultati limitativi
E1. teorema di compattezza, esempi di modelli non standard (2 ore)
E2. aritmetica di Peano, codifica (2 ore)
E3. lemma di punto fisso, teorema di incompletezza di Gödel (2 ore)
E4. funzioni calcolabili, tesi di Church-Turing, teorema di Cantor, esistenza di funzioni incalcolabili (2 ore)
E5. incalcolabilità e incompletezza, esempi: minori di grafi (2 ore)
Rispetto agli obiettivi formativi,
- la parte A1 è specificatamente diretta a formare il necessario linguaggio scientifico per affrontare il corso; tale linguaggio verrà approfondito in tutte le parte successive;
- le parti B1, B3, B5, C1, C3, D4, D5, E2 ed E3 sono principalmente dirette a formare le conoscenze relative all’inferenza logica, con le parti B2 e C2 specificatamente destinate a formare l’abilità di effettuare prove formali;
- le parti B4, B5, B6, C3, D1, D3, D5, E1, E2, E3 ed E5 sono dirette a formare le competenze relative alla capacità di astrazione formale, con qualche sovrapposizione con l’obiettivo precedente ove esso sia funzionale a raccordare le abilità;
- le parti B3, B5, C4, D2, D5 ed E4 sono destinate a consolidare gli obiettivi formativi precedenti in ambito informatico.
Lingua Insegnamento
Italiano
Altre informazioni
Il ricevimento studenti è su appuntamento da concordarsi via email. Il docente risponde solo a email provenienti dall’account universitario del mittente. In caso di necessità, il ricevimento potrà essere effettuato in teleconferenza.
Corsi
Corsi
INFORMATICA
Laurea
3 anni
No Results Found
Persone
Persone
Collaboratori
No Results Found