Logica
A.A. 2018/2019
Obiettivi formativi
L'insegnamento ha lo scopo principale di fornire le conoscenze di base e le capacità di ragionamento proprie della logica matematica. La prima parte dell'insegnamento ha l'obiettivo di descrivere i concetti principali della logica classica: la logica proposizionale e la logica primo ordine. La parte finale fornisce una breve introduzione ad alcune applicazioni della logica all'informatica.
Risultati apprendimento attesi
Le competenze acquisite con l'insegnamento sono la capacità di ragionamento logico, la conoscenza delle principali logiche classiche e la conoscenza di alcune applicazioni della logica all'informatica.
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
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.
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.
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.
Informazioni sul programma
Le competenze acquisite con l'insegnamento sono la capacità di ragionamento logico, la conoscenza delle principali logiche classiche e la conoscenza di alcune applicazioni della logica all'informatica e alla sicurezza informatica.
Prerequisiti
Metodi di accertamento: L'esame consiste in 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.
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.
- 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.
Docente/i
Ricevimento:
Su appuntamento via e-mail
Dipartimento di Informatica - Via Celoria 18 - 20135 - Milano (MI)