Studiare
In questa sezione è possibile reperire le informazioni riguardanti l'organizzazione pratica del corso, lo svolgimento delle attività didattiche, le opportunità formative e i contatti utili durante tutto il percorso di studi, fino al conseguimento del titolo finale.
Piano Didattico
Queste informazioni sono destinate esclusivamente agli studenti e alle studentesse già iscritti a questo corso.Se sei un nuovo studente interessato all'immatricolazione, trovi le informazioni sul percorso di studi alla pagina del corso:
Laurea magistrale in Ingegneria e scienze informatiche - Immatricolazione dal 2025/2026Il piano didattico è l'elenco degli insegnamenti e delle altre attività formative che devono essere sostenute nel corso della propria carriera universitaria.
Selezionare il piano didattico in base all'anno accademico di iscrizione.
1° Anno
2° Anno Attivato nell'A.A. 2021/2022
| Insegnamenti | Crediti | TAF | SSD |
|---|
| Insegnamenti | Crediti | TAF | SSD |
|---|
| Insegnamenti | Crediti | TAF | SSD |
|---|
4 insegnamenti a scelta2 insegnamenti a scelta3 insegnamenti a sceltaLegenda | Tipo Attività Formativa (TAF)
TAF (Tipologia Attività Formativa) Tutti gli insegnamenti e le attività sono classificate in diversi tipi di attività formativa, indicati da una lettera.
Logica in informatica (2020/2021)
Codice insegnamento
4S008914
Docente
Coordinatore
Crediti
6
Offerto anche nei corsi:
- Logica del corso Laurea magistrale in Ingegneria e scienze informatiche [LM-18/32]
Lingua di erogazione
Italiano
Settore Scientifico Disciplinare (SSD)
INF/01 - INFORMATICA
Periodo
II semestre dal 1 mar 2021 al 11 giu 2021.
Obiettivi formativi
Il corso mira a fornire la conoscenza della logica classica e intuizionista (proposizionale e del primo ordine) e del lamba calcolo e della teoria dei tipi. Alla fine del corso gli studenti dovranno dimostrare di possedere le conoscenze necessarie per ragionare all'interno di un sistema logico formale, sia in un ambiente classico che intuizionista. Questa conoscenza consentirà allo studente di: i) eseguire prove formali con un sistema deduttivo; ii) ragionare con sistemi assiomatici. Inoltre gli studenti dovranno sapere come trasferire le nozioni teoriche apprese in contesti logici tipici dell'informatica, come i sistemi di tipo per i linguaggi funzionali. Gli studenti saranno in grado di continuare i loro studi nel campo della logica per l’informatica.
Programma
1. la logica proposizionale:
-proposizioni e connettivi
-semantica
-deduzione naturale
-correttezza e completezza
2. logiche dei predicati:
-quantificatori
-strutture
-tipi di similarità
-semantica
- identità
-deduzione tipi
-correttezza e completezza
3. la normalizzazione in deduzione naturale.
4. confluenza.
5. elementi di teoria dei modelli
-equivalenza, isomorfismo,
6. lambda calcolo senza tipi e con i tipi.
7. il calcolo dei seguenti ed il teorema di cut elimination.
8. Aritmetica di Peano
-primo e secondo teorema di incompletezza
| Autore | Titolo | Casa editrice | Anno | ISBN | Note |
|---|---|---|---|---|---|
| Jean Louis Krivine, Rene Cori | Lambda-calculus, Types and Models | Ellis Horwood | 1993 | 978-0130624079 | |
| van Dalen, Dirk | Logic and Structure. (Edizione 5) | Springer | 2013 | 978-1-4471-4557-8 |
Modalità d'esame
L'esame consiste in un seminario orale della durata approssimativa di 20/30 minuti.
