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.
Tipologia di Attività formativa D e F
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/2026Nella scelta delle attività di tipo D, gli studenti dovranno tener presente che in sede di approvazione si terrà conto della coerenza delle loro scelte con il progetto formativo del loro piano di studio e dell'adeguatezza delle motivazioni eventualmente fornite.
| anni | Insegnamenti | TAF | Docente |
|---|---|---|---|
| 1° 2° | Linguaggio Programmazione Matlab-Simulink | D |
Bogdan Mihai Maris
(Coordinatore)
|
| 1° 2° | Sfide di programmazione | D |
Romeo Rizzi
(Coordinatore)
|
| anni | Insegnamenti | TAF | Docente |
|---|---|---|---|
| 1° 2° | Introduzione alla stampa 3D | D |
Franco Fummi
(Coordinatore)
|
| 1° 2° | Linguaggio programmazione Python | D |
Vittoria Cozza
(Coordinatore)
|
| 1° 2° | Progettazione di componenti hardware su FPGA | D |
Franco Fummi
(Coordinatore)
|
| 1° 2° | Prototipizzazione con Arduino | D |
Franco Fummi
(Coordinatore)
|
| 1° 2° | Tutela dei beni immateriali (SW e invenzione) tra diritto industriale e diritto d’autore | D |
Roberto Giacobazzi
(Coordinatore)
|
| anni | Insegnamenti | TAF | Docente |
|---|---|---|---|
| 1° 2° | Lab.: The fashion lab (1 cfu) | D |
Maria Caterina Baruffi
(Coordinatore)
|
| 1° 2° | Minicorso Blockchain | D |
Nicola Fausto Spoto
(Coordinatore)
|
Ragionamento automatico (2020/2021)
Codice insegnamento
4S02796
Docente
Coordinatore
Crediti
6
Lingua di erogazione
Italiano
Settore Scientifico Disciplinare (SSD)
INF/01 - INFORMATICA
Periodo
II semestre dal 1 mar 2021 al 11 giu 2021.
Obiettivi formativi
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 alle 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.
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.
| Autore | Titolo | Casa editrice | Anno | ISBN | Note |
|---|---|---|---|---|---|
| Bertot, Yves, Castéran, Pierre | Interactive Theorem Proving and Program Development | Springer-Verlag Berlin Heidelberg | 2004 | 978-3-642-05880-6 | |
| 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
Esame scritto
