Logica e informatica (A.A. 2020/2021)
A chi è rivolto il corso. Il corso, di 3 crediti, è una delle sezioni del corso Metodi quantitativi per l'informatica e viene tenuto nel secondo semestre (periodo didattico da marzo 2021 a maggio 2021).
Docente. Prof. Maurizio Lenzerini.
Obiettivi. L'obiettivo del corso è di introdurre la logica matematica come potente strumento per modellare e ragionare formalmente su diversi aspetti dell’informatica, quali: i requisiti di un sistema informatico, i dati, i programmi, gli automi e la computazione in generale. Vengono studiati i principali sistemi formali della logica, in primis la logica proposizionale e la logica dei predicati. Viene affrontato il tema dell’uso della logica nello specificare argomenti, dimostrare o confutare la loro validità ed inferire le loro conseguenze, anche in modo automatico. Vengono poi approfonditi alcuni temi che riguardano l’uso della logica nell’informatica, in particolare nella gestione dei dati, nell’interrogazione di basi di dati, nella specifica di programmi e nel ragionamento sulle proprietà dei programmi e degli automi.
- 27 luglio 2021. Gli studenti che preferiscono sostenere un esame scritto nell'appello di settembre di "Logica e informatica" rispetto alla presentazione di un progetto devono mandare un messaggio di posta elettronica al docente entro il 23 agosto. L'esame si terrà il 1 settembre 2021 alle ore 9:00 in aula 3 in via Ariosto 25, e consisterà nel rispondere a 5 domande relative al programma d'esame. Chi non si prenota entro la data indicata non potrà sostenere l'esame e non ci saranno eccezioni a questa regola.
- 13 aprile 2021. Gli esami della sezione "Logica e informatica" si svolgeranno nella seconda metà di giugno (per l'appello di giugno), nella seconda metà di luglio (per l'appello di luglio), il 1 settembre (lo scritto) e nella seconda metà di settembre (presentazioni di progetti) per l'appello di settembre e nella seconda di ottobre (per l'appello di ottobre).
I periodi per prenotarsi con INFOSTUD per la verbalizzazione dell'esame complessivo di "Metodi quantitativi per l'informatica" saranno rispettivamente il 1-25 giugno 2021 (per l'appello di giugno), 1-25 luglio 2021 (per l'appello di luglio), 1-25 settembre 2021 (per l'appello di settembre) e 1-25 ottobre 2021 (per l'appello di ottobre). Ovviamente al momento della verbalizzazione lo studente deve aver superato l'esame di entrambe le sezioni del corso.
- 20 dicembre 2020. Le lezioni inizieranno venerdì 5 marzo 2021.
- Il materiale didattico prevede le slides preparate dal docente, che si possono scaricare dalla pagina del corso in MOODLE
Per seguire le lezioni a distanza gli studenti che si sono iscritti al corso tramite il sistema MOODLE devono collegarsi alla stanza virtuale ZOOM. Sul sito dell'ateneo è disponibile una pagina che include una guida all'uso di ZOOM. Le registrazioni delle lezioni sono disponibili nella pagina MOODLE del corso.. Gli orari e le aule sono questi:
- mercoledì: [ore 10:00 - 11:00] Sede Marco Polo (RM021), viale dello Scalo S. Lorenzo, 82, aula 106
- venerdì: [ore 08:00 - 10:00] Sede Marco Polo (RM021), viale dello Scalo S. Lorenzo, 82, aula 106
Il materiale delle esercitazioni, comprese le soluzioni degli esercizi, è scaricabile accedendo alla pagina del corso in MOODLE.
| Week | Mercoledì (10:00 - 11:00) aula 106 | Venerdì (08:00 - 10:00) aula 106 |
| 01 (Feb 22) |
|
|
| 02 (Mar 01) |
|
Lezioni 1,2 - Introduzione al corso - Sintassi della logica proposizionale |
| 03 (Mar 08) |
|
Lezioni 3,4 - Semantica della logica proposizionale - Funzioni Booleane e logica proposizionale |
| 04 (Mar 15) | Lezioni 5,6 - La deduzione in logica proposizionale |
|
| 05 (Mar 22) | ||
| 06 (Mar 29) |
|
|
| 07 (Apr 05) | Lezione 7 - Ragionamento in logica proposizionale: definizioni ed esercizi |
Lezioni 8,9 - La nozione di teoria proposizionale |
| 08 (Apr 12) | Lezioni 10,11 - Sistemi di inferenza logica |
|
| 09 (Apr 19) | Lezione 12 - L'algoritmo DPLL per la soddisfacibilità |
Lezioni 13,14 - La logica dei predicati del primo ordine: sintassi |
| 10 (Apr 26) | Lezioni 15,16 - La logica dei predicati del primo ordine: semantica |
|
| 11 (Mag 03) | Lezione 17 - La logica dei predicati del primo ordine: esempi ed esercizi |
Lezioni 18,19 - La logica dei predicati del primo ordine e le basi di dati |
| 12 (Mag 10) | Lezioni 20,21 - Il calcolo relazionale come linguaggio per query e vincoli di integrità |
|
| 13 (Mag 17) | Lezione 22 - Le query congiuntive e la nozione di omomorfismo |
Lezioni 23,24 - Le query congiuntive: containment ed equivalence - Basi di dati deduttive |
| 14 (Mag 24) | Lezioni 25,26 - Il linguaggio Datalog |
- 1. La logica proposizionale. Sintassi e semantica della logica proposizionale. Potere espressivo della logica proposizionale. “Satisfiability”: problema, complessità e algoritmi di decisione. L’inferenza nella logica proposizionale. Problemi e algoritmi di decisione relativi all’inferenza.
- 2. La logica dei predicati del primo ordine. Sintassi e semantica della logica dei predicati del primo ordine. Potere espressivo della logica dei predicati. L’inferenza nella logica dei predicati: deduzione, induzione e abduzione. Sistemi formali per la deduzione. Problemi di decisione nella logica dei predicati. Cenno alle logiche modali e temporali.
- 3. Applicazione della logica nell’informatica. La logica nello sviluppo e nell’analisi dei programmi. Logica e automi. La logica nella gestione dei dati. Logica e linguaggi di interrogazione nelle basi di dati. Il linguaggio Datalog. La logica nella rappresentazione della conoscenza. Linguaggi di programmazione basati sulla logica: il linguaggio Prolog.
- Nel primo caso lo studente o il gruppo di due studenti (non di più) sceglie di affrontare un argomento tra quelli proposti dal docente, e comunica la scelta al docente. Se l'argomento scelto non è stato selezionato già da altri studenti, il docente assegna l'argomento allo studente o al gruppo, altrimenti lo studente o il gruppo dovrà fare un'altra scelta. Alla fine del lavoro svolto lo studente o il gruppo produce una breve relazione (anche semplicemente sotto forma di slides), consegna la relazione al docente pochi giorni prima del colloquio d'esame, e nel colloquio conduce una discussione (tipicamente di una ventina di minuti) sul lavoro svolto. La lista di argomenti viene riportata di seguito (la lista viene continuamente aggiornata fino alla fine del corso):
- Algoritmo per la soddisfacibilità per formule Krom (2-sat): definizione e implementazione (già scelto)
- Algoritmi per la soddisfacibilità per formule Horn: definizione e implementazione (già scelto)
- La deduzione naturale in logica proposizionale (già scelto)
- La tecnica del tableaux per deduzione in logica proposizionale (già scelto)
- Logiche proposizionali modali: sintassi, semantica e deduzione (già scelto)
- Logiche proposizionali temporali: sintassi, semantica e deduzione (già scelto)
- Valutazione e contenimento di query congiuntive estese con unione e negazione (già scelto)
- Formulazione del concetto di macchina di Turing in logica del primo ordine e dimostrazione della indecidibilità dell'implicazione logica al primo ordine mediante riduzione all'halting problem (già scelto)
- Quantified Boolean Formulas (già scelto)
- Adding negation to Datalog (già scelto)
- Disjunctive Datalog (già scelto)
- Formalizzazione di un problema scelto in logica proposizionale in modo che la soluzione del problema corrisponda ad un compito di ragionamento sulle corrispondenti formule proposizionali
- Formalizzazione di un problema scelto in logica del primo ordine in modo che la soluzione del problema corrisponda ad un compito di ragionamento sulle corrispondenti formule del primo ordine
Le possibili date per presentare il lavoro svolto on line all'indirizzo [https://meet.google.com/hzy-save-oqw] sono per il momento le seguenti (altre se ne aggiungeranno per i successivi appelli):
- martedì 18 gennaio 2022, ore 17:00
- martedì 25 gennaio 2022, ore 17:00
- martedì 15 febbraio 2022, ore 17:00
- martedì 22 febbraio 2022, ore 17:00
- Nel secondo caso l'esame consiste di una prova scritta ed eventualmente di una prova orale, entrambe vertenti sul programma d'esame.
- Primo appello: giugno 2021
- Secondo appello: luglio 2021
- Terzo appello: settembre 2021
- Appello straordinario (per studenti studenti part-time, fuori corso, iscritti per l’A.A. 2020-2021 al terzo anno della laurea e al secondo anno della laurea magistrale, studenti con disabilità e con D.S.A.): ottobre 2021
- Quarto appello: gennaio 2022
- Quinto appello: febbraio 2022
- Appello straordinario (per studenti fuori corso, part time, con disabilità e con D.S.A.): aprile 2022