Logica
A.A. 2021/2022
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 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
Primo semestre
Metodi didattici e modalità di erogazione
Saranno disponibili lezioni asincrone (videoregistrazioni o power point con commento audio), organizzate per coprire gli argomenti di ogni lezione dell'insegnamento. Le lezioni registrate saranno rese disponibili settimanalmente sulla piattaforma Ariel dell'insegnamento. Inoltre, negli orari previsti per l'insegnamento, saranno organizzati alcuni incontri sincroni periodici con gli studenti, utilizzando la piattaforma Zoom, al fine di svolgere esercizi, fornire chiarimenti ed approfondimenti e rispondere alle domande degli studenti. Gli incontri sincroni saranno registrati e resi disponibili su Ariel.
Programma e materiale di riferimento
Il programma del corso è invariato. I materiali di riferimento sono invariati. Tutto il materiale didattico di supporto sarà disponibile sempre attraverso la piattaforma Ariel.
Modalità di verifica dell'apprendimento e criteri di valutazione
Gli esami a distanza saranno svolti con l'utilizzo della piattaforma exam.net, con le modalità illustrate sul portale dell'Ateneo. La prova scritta avrà una durata ridotta a circa 60 minuti.
Saranno disponibili lezioni asincrone (videoregistrazioni o power point con commento audio), organizzate per coprire gli argomenti di ogni lezione dell'insegnamento. Le lezioni registrate saranno rese disponibili settimanalmente sulla piattaforma Ariel dell'insegnamento. Inoltre, negli orari previsti per l'insegnamento, saranno organizzati alcuni incontri sincroni periodici con gli studenti, utilizzando la piattaforma Zoom, al fine di svolgere esercizi, fornire chiarimenti ed approfondimenti e rispondere alle domande degli studenti. Gli incontri sincroni saranno registrati e resi disponibili su Ariel.
Programma e materiale di riferimento
Il programma del corso è invariato. I materiali di riferimento sono invariati. Tutto il materiale didattico di supporto sarà disponibile sempre attraverso la piattaforma Ariel.
Modalità di verifica dell'apprendimento e criteri di valutazione
Gli esami a distanza saranno svolti con l'utilizzo della piattaforma exam.net, con le modalità illustrate sul portale dell'Ateneo. La prova scritta avrà una durata ridotta a circa 60 minuti.
Programma
INTRODUZIONE. La logica linguistica, filosofica (studio dei paradossi) e matematica.
LOGICA PROPOSIZIONALE. Sintassi e semantica della logica proposizionale. Sistemi deduttivi del calcolo proposizionale: deduzione naturale e 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: deduzione naturale e 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. Clausole di Horn e programmazione logica.
LOGICA FUZZY. Insiemi fuzzy. Sintassi e semantica della logica fuzzy: cenni.
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: deduzione naturale e 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: deduzione naturale e 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. Clausole di Horn e programmazione logica.
LOGICA FUZZY. Insiemi fuzzy. Sintassi e semantica della logica fuzzy: cenni.
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 del corso.
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 del corso.
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 del corso e la capacità di ragionamento logico. La valutazione è espressa in trentesimi. I risultati della prova saranno comunicati tramite il sistema di verbalizzazione via mail.
Docente/i
Ricevimento:
Su appuntamento via e-mail
Dipartimento di Informatica - Via Celoria 18 - 20135 - Milano (MI)