LOGICA

A.A. di erogazione 2020/2021
Insegnamento obbligatorio

Laurea triennale in INFORMATICA
 (A.A. 2019/2020)

Docenti

Anno di corso: 
2
Tipologia di insegnamento: 
Affine/Integrativa
Sede: 
Como - Università degli Studi dell'Insubria
Settore disciplinare: 
LOGICA MATEMATICA (MAT/01)
Crediti: 
6
Ciclo: 
Secondo Semestre
Ore di attivita' frontale: 
48

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.
Risultati di apprendimento attesi
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 su 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.

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.

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 f consolidare gli obiettivi formativi precedenti in ambito informatico.

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.

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 articolata secondo il seguente schema: (parte A) due domande relative alla presentazione e applicazione delle nozioni presentate nell’insegnamento; (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% dalla conoscenza delle definizioni e dalla capacità di applicarle (parte A), per il 30% dalla conoscenza e comprensione delle dimostrazioni dei teoremi (parte B), per il 40% dalla capacità di applicare le nozioni apprese nel corso alla soluzione degli esercizi (parte C).
Il voto finale è espresso in trentesimi.

Le slides delle lezioni in formato pdf sono disponibili sul sito web del corso, e costituiscono il testo di riferimento. La bibliografia di approfondimento è consigliata ma non obbligatoria, ed è presente nell’ultima slide di ogni lezione.
Sono anche disponibili, sullo stesso sito una collezione di esercizi svolti.

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.

Cerchi il programma? Potrebbe non essere ancora stato caricato o riferirsi ad insegnamenti che verranno erogati in futuro.
Seleziona l‘anno in cui ti sei immatricolato e troverai le informazioni relative all'insegnamento del tuo piano di studio.

A.A. 2020/2021

Anno di corso: 2
Curriculum: PERCORSO COMUNE

A.A. 2019/2020

Anno di corso: 2
Curriculum: PERCORSO COMUNE

A.A. 2018/2019

Anno di corso: 2
Curriculum: PERCORSO COMUNE

A.A. 2017/2018

Anno di corso: 2
Curriculum: PERCORSO COMUNE

A.A. 2016/2017

Anno di corso: 2
Curriculum: PERCORSO COMUNE

A.A. 2015/2016

Anno di corso: 2
Curriculum: PERCORSO COMUNE

A.A. 2014/2015

Anno di corso: 2
Curriculum: PERCORSO COMUNE