Obiettivi:

Scopo del corso è  la presentazione, il più possibile unificante, di alcune logiche di particolare interesse per l'ingegneria della informazione, con particolare attenzione a questioni di decidibilità e agli aspetti applicativi.

Per rispondere alle esigenze culturali di eventuali studenti interessati alla crittografia saranno presentati anche i fondamenti della teoria dei campi finiti, quindi il corso sarà formato da una parte comune e da parti opzionali in alternativa. Sarà quindi tenuto un numero di lezioni ed esercitazioni maggiore di quello previsto dal mix didattico, ma esse saranno organizzate in modo che, seguendo un numero complessivo di ore corrispondente al mix didattico, gli studenti abbiano una completa panoramica del programma più adeguato ai loro interessi.

Gli studenti che vogliano approfondire alcuni aspetti applicativi degli argomenti trattati nel corso, possono sostituire alcune ore di esercitazione con un progetto.

Programma dettagliato

PARTE COMUNE

Logica modale proposizionale: il linguaggio, 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.

PARTI IN ALTERNATIVA

1)

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.

2)

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, applicazioni dei campi finiti.

Prerequisiti

Conoscenze di base di logica matematica ed algebra.

La valutazione sarà effettuata tramite una prova orale. La prova orale potrà essere preceduta da una estemporanea semplice prova scritta. Nel caso lo studente abbia svolto un progetto, il giudizio sul progetto stesso sarà parte integrante della valutazione. 

Eventuali studenti stranieri possono sostenere l'esame in inglese

Dipsense a cura del docente sulle varie parti del corso

Per la parte di logica modale e multimodale

Per la parte di logiche descrittive

Per la parte di campi finiti