ID:
SCV0314
Durata (ore):
48
CFU:
6
SSD:
LOGICA MATEMATICA
Sede:
Como - Università degli Studi dell'Insubria
Anno:
2023
Dati Generali
Periodo di attività
Secondo Semestre (19/02/2024 - 31/05/2024)
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.
Gli obiettivi didattici verranno raggiunti seguendo il seguente schema:
1. ognuno dei cinque capitoli del corso viene introdotto da una discussione generale di inquadramento nelle discipline matematiche e informatiche, con la spiegazione del senso filosofico della materia che si andrà ad affrontare.
2. verranno illustrate le definizioni e i teoremi fondamentali al fine di fornire l’impianto matematico in modo solido e ordinato.
3. esempi di utilizzo accompagneranno i risultati di particolare rilievo, sia per chiarirne il senso, sia per illustrarne l’applicazione.
4. le parti che necessitano (dimostrazioni formali) saranno compendiate da esercizi svolti in classe dal docente, con particolare enfasi sul metodo per la loro risoluzione.
5. al termine di ogni capitolo, si fornisce un sommario dei risultati ottenuti con lo scopo di fornire la prospettiva atta a inquadrarli criticamente sia rispetto al loro senso matematico e informatico, sia in relazione alle conoscenze acquisite in altri corsi.
Gli obiettivi didattici verranno raggiunti seguendo il seguente schema:
1. ognuno dei cinque capitoli del corso viene introdotto da una discussione generale di inquadramento nelle discipline matematiche e informatiche, con la spiegazione del senso filosofico della materia che si andrà ad affrontare.
2. verranno illustrate le definizioni e i teoremi fondamentali al fine di fornire l’impianto matematico in modo solido e ordinato.
3. esempi di utilizzo accompagneranno i risultati di particolare rilievo, sia per chiarirne il senso, sia per illustrarne l’applicazione.
4. le parti che necessitano (dimostrazioni formali) saranno compendiate da esercizi svolti in classe dal docente, con particolare enfasi sul metodo per la loro risoluzione.
5. al termine di ogni capitolo, si fornisce un sommario dei risultati ottenuti con lo scopo di fornire la prospettiva atta a inquadrarli criticamente sia rispetto al loro senso matematico e informatico, sia in relazione alle conoscenze acquisite in altri corsi.
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 due ore articolata secondo il seguente schema: (parte A) 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) due esercizi sullo schema di quelli presentati a lezione.
L’attribuzione del voto finale sarà determinata per il 30% (9/30) dalla conoscenza delle definizioni e dalla capacità di applicarle (parte A), per il 30% (9/30)dalla conoscenza e comprensione delle dimostrazioni dei teoremi (parte B), per il 40% (12/30 ) dalla capacità di applicare le nozioni apprese nel corso alla soluzione degli esercizi (parte C).
Il voto finale è espresso in trentesimi.
L’esame consiste in una prova scritta della durata di due ore articolata secondo il seguente schema: (parte A) 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) due esercizi sullo schema di quelli presentati a lezione.
L’attribuzione del voto finale sarà determinata per il 30% (9/30) dalla conoscenza delle definizioni e dalla capacità di applicarle (parte A), per il 30% (9/30)dalla conoscenza e comprensione delle dimostrazioni dei teoremi (parte B), per il 40% (12/30 ) dalla capacità di applicare le nozioni apprese nel corso alla soluzione degli esercizi (parte C).
Il voto finale è espresso in trentesimi.
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 sito web del corso è: https://marcobenini.me/lectures/logica-informatica/
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.
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