Logica e Informatica (A.A. 2022/2023)


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 febbraio 2023 a maggio 2023).
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.

  • Avvisi
      18 aprile 2023. A causa di improvvisi impegni istituzionali del docente, mercoledì 19 aprile 2023 e venerdì 21 aprile non si terranno le lezioni di Logica e Informatica.

    • 5 febbraio 2023. Le lezioni inizieranno il giorno 24 febbraio 2023.

  • Materiale didattico
    • Il materiale didattico prevede le slides preparate dal docente, che si possono scaricare dalla pagina MOODLE del corso
  • Lezioni: orari e aule

    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 09:00 - 10:00] Sede Marco Polo (RM021), viale dello Scalo S. Lorenzo, 82, aula 106. Le lezioni in questo slot saranno svolte saltuariamente (si veda il calendario qui sotto).
    • venerdì: [ore 13:00 - 15:00] Sede Marco Polo (RM021), viale dello Scalo S. Lorenzo, 82, aula 106
  • Esercitazioni

    Il materiale delle esercitazioni, comprese le soluzioni degli esercizi, è scaricabile accedendo alla pagina MOODLE del corso.

  • Lezioni: calendario e contenuti La lezione del mercoledì viene svolta solo in alcune settimane. Si raccomanda di consultare la tabella per informarsi sui mercoledì in cui ci sarà lezione.
    Settimana Mercoledì (09:00 - 10:00) aula 106 Venerdì (13:00 - 15:00) aula 106
    01 (Feb 20)
    ------
    Lezione 1,2
    - Introduzione al corso
    - Sintassi della logica proposizionale
    02 (Feb 27)
    ------
    Lezione 3,4
    - Semantica della logica proposizionale
    03 (Mar 06)
    ------
    Lezione 5,6
    - Ragionamento in logica proposizionale
    04 (Mar 13) Lezione 7,8
    - Formalizzazione di problemi in logica proposizionale
    Lezione 9,10
    - Inferenza in logica proposizionale
    05 (Mar 20)
    ------
    Lezione 11,12
    - The DP procedure
    06 (Mar 27) Lezione 13,14
    - The DPLL procedure
    Lezione 15,16
    - La tecnica dei tableau per la logica proposizionale
    07 (Apr 03)
    ------
    ------
    08 (Apr 10)
    ------
    Lezione 17,18
    - Introduzione alla logica del primo ordine
    09 (Apr 17)
    ------
    ------
    10 (Apr 24)
    ------
    Lezione 19,20
    - Semantica della logica del primo ordine
    11 (Mag 01) Lezione 21,22
    - Formalizzazione di problemi in logica del primo ordine
    Lezione 23,24
    - Relazione tra logica e basi di dati
    - Calcolo relazionale del primo ordine come linguaggio di query
    12 (Mag 08)
    ------
    Lezione 25,26
    - Vincoli di integrità in logica
    13 (Mag 15) Lezione 27,28
    Le conjunctive query
    Lezione 29,30
    - Il linguaggio Datalog
    14 (Mag 22)
    ------
    ------
  • Programma provvisorio del corso
    • 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.
  • Modalità d'esame
    Lo studente può scegliere di svolgere l'esame per la sezione "Logica e Informatica" tra due modalità:

    • Nel primo caso lo studente o il gruppo di due studenti (non di più) sceglie di affrontare un argomento da essi stessi proposto (eventualmente anche in sinergia con un progetto relativo alla sezione del corso su metodi probabilistici) oppure selezionato 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 dovrà essere fatta un'altra scelta. Una volta ricevuta l'accettazione da parte del docente, lo studente o il gruppo si occupa di reperire il materiale per condurre il lavoro, eventualmente chiedendo consiglio al docente. 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 supportata da slides) sul lavoro svolto. La lista di argomenti viene riportata di seguito (la lista viene continuamente aggiornata fino alla fine del corso):
      • 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
      • Algoritmo per la soddisfacibilità per formule Krom (2-sat): definizione e implementazione
      • Algoritmi per la soddisfacibilità per formule Horn: definizione e implementazione
      • La deduzione naturale in logica proposizionale
      • Implementazione della tecnica del tableaux per deduzione in logica proposizionale
      • Logiche proposizionali modali: sintassi, semantica e deduzione (argomento non più disponibile)
      • Logiche proposizionali temporali: sintassi, semantica e deduzione (argomento non più disponibile)
      • Quantified Boolean Formulas: definizione e tecniche di ragionamento
      • Valutazione di una formula del primo ordine in un'interpretazione finita: studio della complessità
      • 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
      • 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 (argomento non più disponibile)
      • La tecnica del tableaux per la logica del primo ordine
      • Valutazione e contenimento di query congiuntive estese con unione e negazione
      • Algoritmo per la valutazione di programmi Datalog: definizione e dimostrazione di correttezza
      • Datalog con negazione
      • Disjunctive Datalog
      • Description logics
      • Functional dependencies in the relational model

      Quando lo studente è pronto per la presentazione manda un messaggio al docente chiedendo di effettuare la prova in una specifica data tra quelle di seguito indicate. Le possibili date per presentare il lavoro on line all'indirizzo [https://meet.google.com/hzy-save-oqw] sono per il momento le seguenti (altre se ne aggiungeranno nei successivi appelli):

      • martedì 5 settembre 2023, ore 17:00,
      • martedì 12 settembre 2023, ore 17:00,
      • martedì 19 settembre 2023, ore 17:00.
    • Nel secondo caso l'esame consiste di una prova d'esame tradizionale (scritta ed eventualmente orale) vertente sul programma d'esame. Anche in questo caso lo studente deve mandare un messaggio al docente, che indicherà la data dell'esame.
  • Prenotazione degli esami: per la verbalizzazione dell'intero esame di Logica e Metodi Probabilistici dell'Informatica, gli studenti devono utilizzare il servizio del sistema Infostud, prenotandosi ad un appello quando si sono acquisiti entrambi i voti per le due sezioni del corso.
  • Calendario previsto degli esami
    • Primo appello: giugno 2023
    • Secondo appello: luglio 2023
    • Terzo appello: settembre 2023
    • Appello straordinario (per studenti studenti part-time, fuori corso, iscritti per l’A.A. 2022-2023 al terzo anno della laurea e al secondo anno della laurea magistrale, studenti con disabilità e con D.S.A.): ottobre 2023
    • Quarto appello: gennaio 2024
    • Quinto appello: febbraio 2024
    • Appello straordinario (per studenti fuori corso, part time, con disabilità e con D.S.A.): aprile 2024
  • Informazioni sulle edizioni passate del corso
  • Ricevimento studenti. Il martedì alle ore 17 on-line all'indirizzo https://meet.google.com/hzy-save-oqw -- si prega di consultare la sezione delle latest news per eventuali variazioni.