copo del corso è presentare i fondamenti matematici di alcune logiche di particolare interesse per l’Ingegneria dell’Informazione, con particolare attenzione ai problemi di decidibilità, ai metodi di dimostrazione automatica e alle principali applicazioni. Il corso introduce inoltre i fondamenti della teoria dei campi finiti, alla base della moderna crittografia, e alcuni temi di algebra lineare e complessità algebrica, con particolare riferimento ai tensori, al loro rango e alle applicazioni algoritmiche.

Al termine del corso lo studente avrà acquisito una panoramica dei principali risultati relativi alle logiche modali e temporali e dei concetti fondamentali della teoria dei campi finiti, comprendendone il ruolo nelle applicazioni crittografiche e nell’algebra computazionale. Nella parte dedicata ai campi finiti saranno introdotti gli strumenti matematici necessari per comprendere l’aritmetica nei campi finiti, i polinomi irriducibili, le estensioni di campi e alcuni algoritmi fondamentali dell’algebra computazionale, tra cui la Fast Fourier Transform per il prodotto di polinomi e il ruolo dei tensori negli algoritmi per il prodotto di matrici.

Nella parte dedicata alla logica modale, dopo aver presentato i principali risultati di correttezza, completezza e decidibilità per un’ampia classe di logiche modali, verrà illustrato il metodo dei tableaux semantici, alla base di numerosi theorem prover per tali logiche. Saranno infine introdotte le logiche temporali e discusse le logiche CTL, CTL* e LTL, con particolare attenzione al loro impiego nella verifica formale di sistemi concorrenti e reattivi.

Risultati di apprendimento attesi (Descrittori di Dublino)

Al termine del corso lo studente sarà in grado di:

Conoscenza e capacità di comprensione (DdD1)

• comprendere i fondamenti delle logiche modali e temporali, della teoria dei campi finiti e dei principali strumenti di algebra computazionale introdotti nel corso.

Capacità di applicare conoscenza e comprensione (DdD2)

• applicare le tecniche studiate per modellare semplici problemi mediante formalismi logici, svolgere calcoli nei campi finiti e comprendere gli algoritmi fondamentali dell’algebra computazionale e le loro applicazioni.

Autonomia di giudizio (DdD3)

• individuare gli strumenti matematici più appropriati per affrontare un problema e valutarne il corretto ambito di applicazione.

Abilità comunicative (DdD4)

• esporre con rigore e chiarezza i concetti, i risultati e le tecniche presentati nel corso, utilizzando correttamente il linguaggio matematico.

Capacità di apprendimento (DdD5)

• possedere le basi necessarie per approfondire autonomamente argomenti avanzati di logica matematica, algebra e informatica teorica.

La valutazione privilegia non solo la conoscenza di definizioni e risultati teorici, ma anche la capacità di applicare gli strumenti introdotti, argomentare le soluzioni con rigore e utilizzare correttamente il linguaggio matematico.

Il corso tratta argomenti di algebra e di logica matematica che hanno applicazioni dirette all'informatica, ossia la teoria dei campi finiti (crittografia), rudimenti di complessità algebrica (prodotti di polinomi, e tensori per prodotti di matrici) e la logica modale e multimodale (in particolare, le logiche temporali, utilizzate nel model checking). Il corso è suddiviso in due parti.

PRIMA PARTE

Fondamenti di logica modale. Semantica di Kripke. Proprietà della relazione di accessibilità e corrispondenza con i sistemi modali classici (K, S4, S5, KD45). Bisimulazione e invarianza. Logiche multimodali. Logiche epistemiche (K_n, S5_n) e doxastiche (KD45_n). Logiche descrittive (ALC) e corrispondenza con la logica multimodale. Logiche temporali. LTL, CTL e CTL*. Principi di model checking per LTL (basato su automi di Büchi) e CTL (metodo del punto fisso). Introduzione alla logica quantistica. Dai reticoli booleani ai reticoli ortonormali: perché non vale la proprietà distributiva nei sistemi quantistici.

SECONDA PARTE

Monoidi, gruppi e anelli commutativi. Morfismi, ideali, quozienti e teoremi di isomorfismo. Teorema cinese del resto. Anelli di polinomi e algoritmo euclideo. Campi, estensioni, campi di spezzamento e campi finiti. Aritmetica e fattorizzazione di polinomi su campi finiti (algoritmo di Berlekamp). FFT e algoritmi veloci per il prodotto di polinomi. Cenni ai tensori e alle loro applicazioni all’algebra computazionale e agli algoritmi.

• SDG4 - QUALITY EDUCATION

Logica e Algebra 1, Geometria e Algebra lineare, Algoritmi e Principi dell’informatica.

• Prova scritta obbligatoria, con prove in itinere
• Prova orale condizionata (a scelta del docente)

La verifica dell’apprendimento avviene mediante una prova scritta.

Per gli studenti frequentanti è prevista la possibilità di sostenere una prova scritta intermedia sulla parte di Logica (non obbligatoria), svolta a metà semestre. Lo studente che supera tale prova può conservarne l’esito e sostenere la prova scritta relativa alla parte di Algebra al primo appello della sessione invernale al quale si iscrive (gennaio oppure febbraio). Qualora non superi la prova relativa alla parte di Algebra, o desideri rinunciare all’esito della prova intermedia, dovrà sostenere l’intera prova scritta in uno degli appelli ordinari. Negli appelli ordinari la prova scritta riguarda entrambe le parti dell’insegnamento (Logica e Algebra). La prova è costituita da esercizi di applicazione delle tecniche sviluppate durante il corso e da eventuali quesiti teorici volti ad accertare la comprensione dei principali risultati e concetti presentati a lezione.

Il docente si riserva la facoltà di richiedere una prova orale, qualora lo ritenga opportuno ai fini della valutazione finale.

Descrittori di Dublino

La prova d’esame è finalizzata a verificare:

• la conoscenza e la comprensione degli argomenti trattati nel corso;
• la capacità di applicare i metodi e le tecniche apprese alla risoluzione di esercizi e problemi;
• la capacità di utilizzare correttamente il linguaggio e il formalismo matematico;
• l’autonomia nell’impostazione e nello sviluppo delle soluzioni ai problemi proposti.

Per la la parte di campi finiti.

Per la la parte di campi finiti.

Per la parte di tensori.

Per la parte di logica modale.

Per la parte di logica modale.

Per la parte di logica modale.