Logica
A.A. 2023/2024
Obiettivi formativi
L'obiettivo dell'insegnamento è di fornire le conoscenze di base e le capacità di ragionamento proprie della Logica e di introdurre le applicazioni della Logica alla Sicurezza Informatica.
Risultati apprendimento attesi
Al termine dell'insegnamento, lo studente dovrà essere in grado di modellare e risolvere semplici problemi, logici o di Sicurezza Informatica, con gli strumenti e le tecniche presentate nell'insegnamento.
Periodo: Primo semestre
Modalità di valutazione: Esame
Giudizio di valutazione: voto verbalizzato in trentesimi
Corso singolo
Questo insegnamento può essere seguito come corso singolo.
Programma e organizzazione didattica
Edizione unica
Responsabile
Periodo
Primo semestre
Programma
INTRODUZIONE. La logica linguistica, filosofica (studio dei paradossi) e matematica.
LOGICA PROPOSIZIONALE. Sintassi e semantica della logica proposizionale. Sistemi deduttivi del calcolo proposizionale: calcolo dei sequenti. Forme normali congiuntive e disgiuntive. Cenni di complessità computazionale di alcuni problemi di logica proposizionale.
LOGICA PREDICATIVA. Sintassi e semantica della logica dei predicati. Sistemi deduttivi del calcolo predicativo: calcolo dei sequenti. Forma normale prenessa e forma di Skolem. Semidecibilità della logica predicativa. Traduzione dal linguaggio naturale.
RISOLUZIONE. Algoritmo di unificazione. Metodi di risoluzione proposizionale e predicativa.
BINARY DECISION DIAGRAMS (OBDD). La rappresentazione di funzioni booleane con OBDD. Riduzione di un OBDD. Operatori logici e la funzione Apply.
VERIFICA FORMALE DI PROGRAMMI. Triple di Hoare. Regole di calcolo per la correttezza parziale di programmi. Regole di calcolo per la correttezza totale di programmi.
LOGICHE MODALI. Sintassi e semantica delle logiche modali. Esempi di logiche modali. Modello di Kripke.
LOGICA PER LA SICUREZZA. Sintassi e semantica della logica di BAN. Analisi del Protocollo di Needham-Schroeder.
LOGICA PROPOSIZIONALE. Sintassi e semantica della logica proposizionale. Sistemi deduttivi del calcolo proposizionale: calcolo dei sequenti. Forme normali congiuntive e disgiuntive. Cenni di complessità computazionale di alcuni problemi di logica proposizionale.
LOGICA PREDICATIVA. Sintassi e semantica della logica dei predicati. Sistemi deduttivi del calcolo predicativo: calcolo dei sequenti. Forma normale prenessa e forma di Skolem. Semidecibilità della logica predicativa. Traduzione dal linguaggio naturale.
RISOLUZIONE. Algoritmo di unificazione. Metodi di risoluzione proposizionale e predicativa.
BINARY DECISION DIAGRAMS (OBDD). La rappresentazione di funzioni booleane con OBDD. Riduzione di un OBDD. Operatori logici e la funzione Apply.
VERIFICA FORMALE DI PROGRAMMI. Triple di Hoare. Regole di calcolo per la correttezza parziale di programmi. Regole di calcolo per la correttezza totale di programmi.
LOGICHE MODALI. Sintassi e semantica delle logiche modali. Esempi di logiche modali. Modello di Kripke.
LOGICA PER LA SICUREZZA. Sintassi e semantica della logica di BAN. Analisi del Protocollo di Needham-Schroeder.
Prerequisiti
Nessuno.
Metodi didattici
Lezioni frontali.
Materiale di riferimento
- Andrea Asperti, Agata Ciabattoni, Logica a Informatica McGraw-Hill, 1997.
- Michael Huth , Mark Ryan. Logic in Computer Science: modelling and reasoning about systems (2nd edition), Cambridge University Press, 2004.
- Lucidi ed altro materiale disponibile sul sito web dell'insegnamento.
La pagina web dell'insegnamento è: https://vcirianil.ariel.ctu.unimi.it
- Michael Huth , Mark Ryan. Logic in Computer Science: modelling and reasoning about systems (2nd edition), Cambridge University Press, 2004.
- Lucidi ed altro materiale disponibile sul sito web dell'insegnamento.
La pagina web dell'insegnamento è: https://vcirianil.ariel.ctu.unimi.it
Modalità di verifica dell’apprendimento e criteri di valutazione
L'esame è una prova scritta. La prova scritta richiede la soluzione di esercizi di tipo applicativo e teorico, aventi contenuti e difficoltà analoghi a quelli affrontati nelle lezioni. Durante lo scritto non è ammessa la consultazione di testi o appunti. I parametri di valutazione comprendono: la conoscenza degli argomenti dell'insegnamento e la capacità di ragionamento logico. La valutazione è espressa in trentesimi. I risultati della prova saranno comunicati tramite il sistema di verbalizzazione via mail.
Siti didattici
Docente/i
Ricevimento:
Su appuntamento via e-mail
Dipartimento di Informatica - Via Celoria 18 - 20135 - Milano (MI)