logo-polimi
Loading...
Risorse bibliografiche
Risorsa bibliografica obbligatoria
Risorsa bibliografica facoltativa
Scheda Riassuntiva
Anno Accademico 2018/2019
Scuola Scuola di Ingegneria Industriale e dell'Informazione
Insegnamento 091021 - LOGICA E ALGEBRA 2
Docente Frigeri Achille
Cfu 5.00 Tipo insegnamento Monodisciplinare

Corso di Studi Codice Piano di Studio preventivamente approvato Da (compreso) A (escluso) Insegnamento
Ing Ind - Inf (Mag.)(ord. 270) - MI (481) COMPUTER SCIENCE AND ENGINEERING - INGEGNERIA INFORMATICA*AZZZZ091021 - LOGICA E ALGEBRA 2

Obiettivi dell'insegnamento

Scopo del corso è la presentazione, il più possibile unificante, di alcune logiche di particolare interesse per l'Ingegneria dell'Informazione, con particolare attenzione a questioni di decidibilità e agli aspetti applicativi, nonché la discussione di alcuni dei fondamenti matematici della crittografia, ovvero la teoria dei campi finiti.

 

Alla fine del corso lo studente dovrebbe avere a disposizione un'ampia panoramica sui risultati principali relativi alle logiche modali e temporali, sulle principali famiglie di logiche descrittive e sui concetti della teoria dei campi finiti legati alle applicazioni in ambito crittografico.

 

Nella prima parte, dopo i principali risultati di corretteza, completezza e decidibilità per un'ampia classe di logiche modali, verrà descritto il procedimento di risoluzione tramite i tableaux semantici. Tale algoritmo è alla base dei principali theorem prover per le logiche modali: uno di esso verrà brevemente presentato nel corso di una esercitazione. Verranno poi introdotte le logiche temporali e discusse le logiche CTL, CTL* e LTL. Per la logica LTL verrà presentato il model checking basato su automi. Anche in questo caso verrà presentato l'algoritmo e un programma per la verifica automatica.

 

Nella parte dedicata alle logiche descrittive verranno presentate le principali famiglie di questo tipo di logiche, con particolare riguardo alla loro espressività e alla loro decidibilità. Anche in questo caso verranno discussi alcuni algoritmi di decisione (nel caso di logiche decidibili) e discussa brevemente la loro complessità.

 

Nella parte dedicata ai campi finiti verranno introdotti i concetti di base su cui si fondano le moderne tecniche crittografiche. Verrà presentato il principale algoritmo di fattorizzazione (algoritmo di Berlekamp). Verranno discusse alcune applicazioni, con particolare riferimento ai protocolli di firma digitale e ai registri a scorrimento a retroazione lineare.


Risultati di apprendimento attesi

Le lezioni e le esercitazioni consentiranno allo studente di

- conoscere e comprendere (DdD1):

- i concetti chiave degli argomenti trattati: la semantica di Kripke, i sistemi normali di logica modale, le estensioni di campi finiti e le principali tecniche dimostrative relative a tali argomenti;

-i principali formalismi logici di principale interesse per l'Ingegneria dell'Informazione: logiche modali, temporali e descrittive;

-la nozione di sistema normale e di dimostrazione, nonché la differenza tra "dimostrabile" e "vero";

-la struttura di anello e campo e di campo di spezzamento su un anello di polinomi.

- saper applicare le conoscenza acquisite al fine di (DdD2):

- saper analizzare un problema al fine di individuare il formalismo logico più adatto alla sua descrizione;

- avere la capacità di modellare un problema in un nel linguaggio logico scelto;

- avere la capacità di comprendere il funzionamento di un theorem prover per logiche modali, descrittive o temporali e aver le basi per saperlo progettare e utilizzare;

- comprendere i concetti matematici che stanno alla base di alcune applicazioni crittografiche e avere le basi per progettare o utilizzare sofware dedicati.

- avere una capacità di apprendimento (DdD5):

- che permetta di comprendere concetti chiave e nozioni avanzate nell'ambito della Logica e dell'Algebra applicata all'Informatica;

- che permetta allo studente di sviluppare una forma mentis orientata al rigore di pensiero e migliorare il processo di astrazione di un problema;

- che, in virtù dei punti precedenti, permetta allo studente che lo voglia di approfondire in modo autonomo argomenti avanzati o di ricerca relativi alle applicazioni matematiche all'Informatica.

Dunque il docente si attende una comprensione non limitata all'enunciazione di definizioni e risultati o all'applicazione di tecniche standard, ma una valutazione critica, ovvero la capacità di distinguere tra diverse situazioni e di compiere scelte consapevoli ad esempio nell'ambito della modellizzazione di un problema. Ci si aspetta infine un'esposizione ben argomentata della teoria supportate da argomentazioni matematiche. 


Argomenti trattati

Il corso tratta alcune logiche di particolare interesse per l'Ingegneria dell'Informazione, con particolare attenzione a questioni di decidibilità e agli aspetti applicativi. Per rispondere alle esigenze culturali degli studenti interessati ai fondamenti matematici della crittografia saranno presentati anche i concetti base della teoria dei campi finiti.

 

PRIMA PARTE

 

Logica modale proposizionale: sintassi, semantica di Kripke, sistemi normali di logica modale, modelli standard canonici, correttezza e completezza, filtrazioni e decidibilità. Tableaux. Applicazioni.

Logica temporale: la logica temporale come particolare logica normale bimodale, logiche temporali lineari, assiomi che distinguono la granularità del tempo. La logica determinata dal frame (w,<): correttezza, completezza e decidibilità.  LTL, CTL, CTL* ed applicazioni al model checking. Cenni sulla logica dinamica. Applicazioni.

 

SECONDA PARTE

 

Complementi di logica modale: Sistemi di logiche modali classiche e modelli minimali. Cenni alle logiche modali del I ordine.

Logiche descrittive: Definizione delle logiche descrittive, gli A-box e i T-box, servizi di reasoning nelle logiche descrittive. Classificazione e potere espressivo di diverse logiche descrittive. Applicazioni.

 

TERZA PARTE

 

Campi finiti: Richiami di teoria delle principali strutture algebriche (gruppi, anelli, campi), anelli di polinomi, estensioni di campi, struttura dei campi finiti (caratterizzazione dei campi finiti, algoritmi relativi), polinomi a coefficienti in campi finiti e loro fattorizzazione: l'algoritmo di Berlekamp. Applicazioni dei campi finiti: la firma digitale e i registri a scorrimento a retroazione lineare.

 

 


Prerequisiti

Conoscenze di base di logica matematica, algebra ed informatica teorica.


Modalità di valutazione

La valutazione sarà effettuata tramite una prova orale (teoremi e dimostrazioni) su argomenti preventivamente concordati con lo studente relativi a due su tre delle parti del corso (obbligatoria quella relativa alle logiche modali, e una a scelta tra quella relativa alle logiche descrittive e quella relativa ai campi finiti). In alternativa sarà possibile anche lo svolgimento di un approfondimento per ciascuna delle due parti scelte. Si può anche optare per una modalità mista: la prova orale per una delle due parti del corso, l'approfondimento per l'altra. Gli approfondimenti verranno concordati con lo studente: potrà essere scelto all'interno di una lista presente sulla pagina BeeP del corso o direttamente proposto dallo studente.

 

L'approfondimento può essere svolto tramite una presentazione alla lavagna, oppure tramite la discussione di una tesina preventivamente consegnata al docente, oppure tramite la discussione di una presentazione video preventivamente caricata su un servizio di video sharing (youtube). 

 

Eventuali studenti stranieri possono sostenere l'esame in inglese.


Bibliografia
Risorsa bibliografica obbligatoriaNote di lezioni ed esercitazioni del corso https://beep.metid.polimi.it/web/2017-18-logica-e-algebra-2-achille-frigeri-/documenti-e-media
Note:

Dispense a cura del docente sulle varie parti del corso

Risorsa bibliografica facoltativaBrian F. Chellas, Modal Logic : An Introduction, Editore: Cambridge University Press, Anno edizione: 1980, ISBN: 9780511621192 https://beep.metid.polimi.it/web/2017-18-logica-e-algebra-2-achille-frigeri-/documenti-e-media
Risorsa bibliografica facoltativaR.Goldblatt, Logics of time and computation, Editore: CSLI, Anno edizione: 1992, ISBN: 0937073946 http://phil.gu.se/logic/books/Goldblatt:Logics_of_time_and_computation.pdf
Note:

Per la parte di logica modale e multimodale

Risorsa bibliografica facoltativaCapitolo 2 di The Description Logic Handbook http://www.inf.unibz.it/%7Efranconi/dl/course/dlhb/dlhb-02.pdf.
Note:

Per la parte di logiche descrittive

Risorsa bibliografica facoltativaR.Lidl, H.Niederreiter, Introduction to finite fields and their applications, Editore: Cambridge University Press, Anno edizione: 1994, ISBN: 0521460948
Note:

Per la parte di campi finiti


Forme didattiche
Tipo Forma Didattica Ore di attività svolte in aula
(hh:mm)
Ore di studio autonome
(hh:mm)
Lezione
30:00
45:00
Esercitazione
20:00
30:00
Laboratorio Informatico
0:00
0:00
Laboratorio Sperimentale
0:00
0:00
Laboratorio Di Progetto
0:00
0:00
Totale 50:00 75:00

Informazioni in lingua inglese a supporto dell'internazionalizzazione
Insegnamento erogato in lingua Italiano
Disponibilità di materiale didattico/slides in lingua inglese
Disponibilità di libri di testo/bibliografia in lingua inglese
Possibilità di sostenere l'esame in lingua inglese
Disponibilità di supporto didattico in lingua inglese
schedaincarico v. 1.6.1 / 1.6.1
Area Servizi ICT
26/01/2020