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.

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/2026

Il 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.

CURRICULUM TIPO:

1° Anno 

2° Anno   Attivato nell'A.A. 2023/2024

InsegnamentiCreditiTAFSSD
Prova finale
24
E
-
Attivato nell'A.A. 2023/2024
InsegnamentiCreditiTAFSSD
Prova finale
24
E
-
Insegnamenti Crediti TAF SSD
Tra gli anni: 1°- 2°
2 insegnamenti a scelta (A.A. 2022/23: Quantum computing non erogato; A.A. 2023/24: Progettazione ad alte prestazioni in C++ non erogato)
6
B
INF/01
6
B
INF/01
Tra gli anni: 1°- 2°
Lingua inglese liv. B2
3
F
-
Tra gli anni: 1°- 2°
Tra gli anni: 1°- 2°
Altre attivita'
3
F
-

Legenda | 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.




S Stage e tirocini presso imprese, enti pubblici o privati, ordini professionali

Codice insegnamento

4S010508

Coordinatore

Andrea Masini

Crediti

6

Lingua di erogazione

Italiano

Settore Scientifico Disciplinare (SSD)

INF/01 - INFORMATICA

Periodo

Secondo semestre dal 6 mar 2023 al 16 giu 2023.

Obiettivi di apprendimento

Scopo del corso è quello di fornire un’introduzione alle tecniche di meccanizzazione del ragionamento logico, utilizzando strumenti basati su sistemi di deduzione automatica o strumenti di assistenza alla dimostrazione. Particolare rilevanza verrà dato sia al problema della formalizzazione che a quello della verifica/dimostrazione di proprietà, usando sistemi goal-driven. Alla fine del corso gli studenti sapranno affrontare la formalizzazione e verifica automatica usando o ragionatori automatici oppure proof-assistant. Gli studenti saranno in grado di proseguire gli studi nell’ambito del ragionamento meccanico ad esempio sviluppando tesi magistrali.

Prerequisiti e nozioni di base

Nozioni di base di logica

Programma

Parte 1- Fondazioni
Richiami di deduzione naturale (classica ed intuizionista)
Lambda calcolo tipato semplice.
Type checking e type inference.
Il sistema F ed il Calcolo delle Costruzioni.
Cenni alla deduzione automatica in logica proposizionale.
Parte 2 - Il sistema Coq
Semplici dimostrazioni in Coq (Goal, assunzioni e tattiche).
Programmazione funzionale in CoQ.
Tipi di dato strutturati.
Polimorfismo e funzioni di ordine superiore.
Le tattiche
Logica in CoQ.
Induzione e co-induzione.

Modalità didattiche

Lezioni frontali e interattive.

Modalità di verifica dell'apprendimento

Per superare l'esame, deve essere realizzato un progetto che verrà assegnato un mese prima del primo appello.
Ogni progetto può essere realizzato da un gruppo di una o due persone.
Il progetto deve essere scritto in Coq (con il codice adeguatamente commentato) ed essere accompagnato da una relazione di poche pagine.
Ogni progetto può essere realizzato usando i costrutti e tattiche viste a lezione. Ogni e costrutto e tattica utilizzata e non spiegata a lezione deve essere spiegata nella relazione di accompagnamento.
L'esame consisterà in una prova orale in cui verrà discusso il progetto svolto.

Le/gli studentesse/studenti con disabilità o disturbi specifici di apprendimento (DSA), che intendano richiedere l'adattamento della prova d'esame, devono seguire le indicazioni riportate QUI

Criteri di valutazione

Verrà valutato:
1) la realizzazione del progetto;
2) l'orale in cui viene discusso il progetto.

Criteri di composizione del voto finale

Il voto finale sarà basato su come è stato realizzato il progetto e su come le/gli esaminande/i risponderanno alle domande in sede di orale.

Lingua dell'esame

Italiano