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

A.A. 2024/2025 A.A. 2023/2024 A.A. 2022/2023 A.A. 2021/2022 A.A. 2020/2021 A.A. 2019/2020 A.A. 2018/2019 A.A. 2017/2018 A.A. 2016/2017 A.A. 2015/2016 A.A. 2014/2015 A.A. 2013/2014 A.A. 2012/2013 A.A. 2011/2012 A.A. 2010/2011 A.A. 2009/2010

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. 2021/2022

InsegnamentiCreditiTAFSSD
Prova finale
24
E
-
Attivato nell'A.A. 2021/2022
InsegnamentiCreditiTAFSSD
Prova finale
24
E
-
Insegnamenti Crediti TAF SSD
Tra gli anni: 1°- 2°
12
B
ING-INF/05
Tra gli anni: 1°- 2°
12
B
ING-INF/05
Tra gli anni: 1°- 2°
4 insegnamenti a scelta
6
B
ING-INF/05
6
B
ING-INF/05
6
B
ING-INF/05
6
B
ING-INF/05
6
B
ING-INF/05
6
B
ING-INF/05
Tra gli anni: 1°- 2°
2 insegnamenti a scelta
6
B
INF/01
6
B
INF/01
6
B
INF/01
6
B
INF/01
6
B
INF/01
6
B
INF/01
6
B
INF/01
6
B
INF/01
6
B
INF/01
6
B
INF/01
6
B
INF/01
6
B
INF/01
6
B
INF/01
6
B
INF/01
6
B
INF/01
6
B
INF/01
6
B
INF/01
6
B
INF/01
6
B
INF/01
6
B
INF/01
Tra gli anni: 1°- 2°
3 insegnamenti a scelta
6
C
INF/01
6
C
INF/01
6
C
INF/01
6
C
INF/01
6
C
INF/01
6
C
INF/01
6
C
INF/01
6
C
INF/01
6
C
SECS-P/10
6
C
INF/01
6
C
INF/01
6
C
INF/01
6
C
INF/01
6
C
INF/01
6
C
INF/01
6
C
INF/01
6
C
INF/01
6
C
INF/01
6
C
INF/01
6
C
INF/01
6
C
INF/01
Tra gli anni: 1°- 2°
Lingua inglese competenza linguistica - liv. B2
3
F
-
Tra gli anni: 1°- 2°
12
D
-
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.

A Attività di base
B Attività caratterizzanti
C Attività formative affini o integrative
D Attività a scelta dello studente
E Prova finale
F Altre attività formative
S Stage e tirocini presso imprese, enti pubblici o privati, ordini professionali

Ragionamento automatico  (2020/2021)

Codice insegnamento

4S02796

Docente

Andrea Masini

Coordinatore

Andrea Masini

Crediti

6

Lingua di erogazione

Italiano

Settore Scientifico Disciplinare (SSD)

INF/01 - INFORMATICA

Periodo

II semestre dal 1 mar 2021 al 11 giu 2021.

Orario Lezioni MoodleMoodle Seminari 0

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.

Testi di riferimento
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

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