Docente
- Giovanna D'Agostino
Finalità del corso.
Fornire approfondite competenze teoriche e metodologiche nelle aree fondamentali delle applicazioni della Logica Matematica all'Informatica, in particolare nel campo della deduzione automatica e a quello della verifica dei sistemi informatici.
In particolare, lo studente dovra': raggiungere un'adeguata conoscenza di uno o piu' calcoli per la logica classica e delle problematiche legate alla deduzione automatica; conoscere gli aspetti semantici e dimostrativi delle principali logiche utilizzate nella verifica dei sistemi informatici (logiche modali e temporali, logiche al
second'ordine) con particolare attenzione alle questioni di correttezza, completezza, decidibilita' e potere espressivo; riconoscere le connessioni che le tematiche sopra
riportate hanno con altri aspetti della Logica, come la teoria dei giochi e la teoria dei modelli / modelli finiti.
Per poter seguire il corso con profitto, occorre avere una conoscenza di base
della sintassi, della semantica e delle regole di derivazione della logica al prim'ordine, come vengono studiate di regola in un primo corso di Logica Matematica della laurea triennale in Informatica o in Matematica. Se non si e' seguito un corso di questo genere alla laurea triennale, si consiglia vivamente di studiare le dispense del corso di Logica Matematica della Laurea triennale di Informatica di Udine,
reperibili al sito
http://users.dimi.uniud.it/~alberto.marcone/LM1.html
Breve introduzione al corso