Logic of computation and information
A.A. 2020/2021
Obiettivi formativi
By locating computational and information systems in their conceptual and technical evolution, students will gain working knowledge of the underlying logics and will understand how they are used for many applications in other sciences. The course includes activities for understanding different formal models of computation and for the representation of information transmission, both single and multi-agent. Such notions and methods will be valuable in any activity requiring advanced reasoning and problem-solving abilities in the computational domain.
Risultati apprendimento attesi
Knowledge acquisition and understanding:
The course provides knowledge of formal methods and logics in the area of computing and information essential for the analysis and understanding of new software and data-intensive science methodologies. The course provides basic knowledge and technical skills in the following topics:
- Logic and computability
- Turing Computability
- Logics of Program Correctness
- Process Algebra
- Temporal Logics
- Logics of Information
- Multi-Agent Systems
Skills acquisition and ability to apply knowledge:
At the end of the course, students are expected to be able to:
- formally identify classes of computable functions and problems;
- formally define properties of computational processes;
- formally express reasoning about computational processes;
- formally describe informational structures and reasoning on them.
The course provides knowledge of formal methods and logics in the area of computing and information essential for the analysis and understanding of new software and data-intensive science methodologies. The course provides basic knowledge and technical skills in the following topics:
- Logic and computability
- Turing Computability
- Logics of Program Correctness
- Process Algebra
- Temporal Logics
- Logics of Information
- Multi-Agent Systems
Skills acquisition and ability to apply knowledge:
At the end of the course, students are expected to be able to:
- formally identify classes of computable functions and problems;
- formally define properties of computational processes;
- formally express reasoning about computational processes;
- formally describe informational structures and reasoning on them.
Periodo: Secondo semestre
Modalità di valutazione: Esame
Giudizio di valutazione: voto verbalizzato in trentesimi
Corso singolo
Questo insegnamento non può essere seguito come corso singolo. Puoi trovare gli insegnamenti disponibili consultando il catalogo corsi singoli.
Programma e organizzazione didattica
Edizione unica
Responsabile
Periodo
Secondo semestre
Durante la fase di didattica emergenziale, il programma viene mantenuto con le seguenti modifiche necessarie per una buona fruizione online del corso originariamente progettato per la didattica in presenza.
Ambienti on-line utilizzati:
Ariel: https://gprimierolci.ariel.ctu.unimi.it/
Moodle: link presente in Ariel
Teams: codice presente in Ariel
Metodi didattici:
Le lezioni si terranno in base agli scenari di rischio:
- massima gravità (zona rossa): le lezioni si terranno solo a distanza in modalità sincrona (in Teams)
- elevata gravità (zona arancione): le lezioni si terranno in modalità mista, parte in presenza e parte on line.
Le lezioni in presenza si terranno in modalità duale permettendo la partecipazione anche agli studenti a distanza (collegati in in Teams). Le lezioni a distanza si terranno in modalità sincrona (in Teams)
- gravità (zona gialla): le lezioni si terranno con le medesime modalità della zona arancione e, se vi saranno le condizioni, verrà aumentato il numero di lezioni tenute in presenza.
Il calendario delle lezioni in presenza e gli aggiornamenti saranno pubblicati nel corso on line in Ariel/Moodle. Il materiale didattico e le registrazioni delle lezioni verranno rese disponibili online sul sito Ariel/Moodle del corso.
Modalità di verifica dell'apprendimento e criteri di valutazione:
L'esame è scritto e viene svolto in Teams/Moodle SEB in tutti gli stati di emergenza (zona gialla, arancione e rossa), secondo le indicazioni fornite dall'Ateneo.
Gli studenti che intendono partecipare alle lezioni in presenza devono fare riferimento alle disposizioni dell'Ateneo:
https://www.unimi.it/it/studiare/frequentare-un-corso-di-laurea/seguire-il-percorso-di-studi/didattica-presenza
Gli studenti che intendono partecipare alle lezioni in Teams devono fare riferimento alle seguenti guide tecniche:
https://www.unimi.it/it/studiare/servizi-gli-studenti/servizi-tecnologici-e-online/microsoft-office-365-education
Per partecipare alle sessioni di esame gli studenti devono fare riferimento alle seguenti indicazioni
https://www.unimi.it/it/studiare/frequentare-un-corso-di-laurea/seguire-il-percorso-di-studi/esami/esami-distanza-faq-gli-studenti
Ambienti on-line utilizzati:
Ariel: https://gprimierolci.ariel.ctu.unimi.it/
Moodle: link presente in Ariel
Teams: codice presente in Ariel
Metodi didattici:
Le lezioni si terranno in base agli scenari di rischio:
- massima gravità (zona rossa): le lezioni si terranno solo a distanza in modalità sincrona (in Teams)
- elevata gravità (zona arancione): le lezioni si terranno in modalità mista, parte in presenza e parte on line.
Le lezioni in presenza si terranno in modalità duale permettendo la partecipazione anche agli studenti a distanza (collegati in in Teams). Le lezioni a distanza si terranno in modalità sincrona (in Teams)
- gravità (zona gialla): le lezioni si terranno con le medesime modalità della zona arancione e, se vi saranno le condizioni, verrà aumentato il numero di lezioni tenute in presenza.
Il calendario delle lezioni in presenza e gli aggiornamenti saranno pubblicati nel corso on line in Ariel/Moodle. Il materiale didattico e le registrazioni delle lezioni verranno rese disponibili online sul sito Ariel/Moodle del corso.
Modalità di verifica dell'apprendimento e criteri di valutazione:
L'esame è scritto e viene svolto in Teams/Moodle SEB in tutti gli stati di emergenza (zona gialla, arancione e rossa), secondo le indicazioni fornite dall'Ateneo.
Gli studenti che intendono partecipare alle lezioni in presenza devono fare riferimento alle disposizioni dell'Ateneo:
https://www.unimi.it/it/studiare/frequentare-un-corso-di-laurea/seguire-il-percorso-di-studi/didattica-presenza
Gli studenti che intendono partecipare alle lezioni in Teams devono fare riferimento alle seguenti guide tecniche:
https://www.unimi.it/it/studiare/servizi-gli-studenti/servizi-tecnologici-e-online/microsoft-office-365-education
Per partecipare alle sessioni di esame gli studenti devono fare riferimento alle seguenti indicazioni
https://www.unimi.it/it/studiare/frequentare-un-corso-di-laurea/seguire-il-percorso-di-studi/esami/esami-distanza-faq-gli-studenti
Programma
1. Computazione e Decidibilità
2. Computazione meccanica
3. Logiche per la Correttezza di Programmi
4. Elementi di Algebra dei Processi
5. Logiche Temporali
6. Logiche dell'informazione
7. Sistemi Multi-Agente
8. Logiche per la Comunicazione
2. Computazione meccanica
3. Logiche per la Correttezza di Programmi
4. Elementi di Algebra dei Processi
5. Logiche Temporali
6. Logiche dell'informazione
7. Sistemi Multi-Agente
8. Logiche per la Comunicazione
Prerequisiti
Il completamento di almeno un corso di logica è fortemente raccomandato.
Metodi didattici
Lezioni frontali ed esercitazioni.
Materiale di riferimento
G.Primiero. On the Foundations of Computing. OUP, 2019. [selected chapters]
M.Huth, M.Ryan, Logic in Computer Science, CUP 2004. [selected chapters]
C. Bayer, J.P. Katoen, Principles of Model-Checking, MIT Press, 2008. [selected chapters]
L. Floridi, The Logic of Being Informed, Logique Et Analyse, vol 196, pp. 433-460 (2006)
P. Allo, The Logic of Being Informed Revisited and Revised, Philosophical Studies, 153(53), pp.417-434 (2011)
G.Primiero, An Epistemic Logic for Becoming Informed, Synthese, 167:2, pp.363-389, 2009.
M. D'Agostino, An informational view of Classical Logic, Theoretical Computer Science, vol. 606, pp. 79-97, 2015.
G. Primiero, A logic of negative trust, Journal of Applied Non-Classical Logic, 2020 https://doi.org/10.1080/11663081.2020.1789404.
M.Huth, M.Ryan, Logic in Computer Science, CUP 2004. [selected chapters]
C. Bayer, J.P. Katoen, Principles of Model-Checking, MIT Press, 2008. [selected chapters]
L. Floridi, The Logic of Being Informed, Logique Et Analyse, vol 196, pp. 433-460 (2006)
P. Allo, The Logic of Being Informed Revisited and Revised, Philosophical Studies, 153(53), pp.417-434 (2011)
G.Primiero, An Epistemic Logic for Becoming Informed, Synthese, 167:2, pp.363-389, 2009.
M. D'Agostino, An informational view of Classical Logic, Theoretical Computer Science, vol. 606, pp. 79-97, 2015.
G. Primiero, A logic of negative trust, Journal of Applied Non-Classical Logic, 2020 https://doi.org/10.1080/11663081.2020.1789404.
Modalità di verifica dell’apprendimento e criteri di valutazione
Per studenti frequentanti e non frequentanti: esame scritto al termine del corso. L'esame include domande aperte (30%), esercizi (50%) e test a risposta multipla (20%). Queste proporzioni riflettono il contributo di ciascuna tipologia alla composizione del voto finale. Test a risposta multipla e domande a risposta aperta mirano ad una verifica della comprensione dei concetti e delle definizioni, gli esercizi sono formulati per valutare la capacità di risoluzione di problemi. Opzionale in aggiunta al test: un progetto da sviluppare a fine corso su un tema e con modalità concordate.
Moduli o unità didattiche
Unita' didattica A
M-FIL/02 - LOGICA E FILOSOFIA DELLA SCIENZA - CFU: 3
Lezioni: 20 ore
Unita' didattica B
M-FIL/02 - LOGICA E FILOSOFIA DELLA SCIENZA - CFU: 3
Lezioni: 20 ore
Unita' didattica C
M-FIL/02 - LOGICA E FILOSOFIA DELLA SCIENZA - CFU: 3
Lezioni: 20 ore
Docente/i
Ricevimento:
Martedì, ore 14:00-17:00. Gli studenti sono sempre pregati di contattare il docente per email per confermare data e ora.
Teams/Slack