- Docente: Ugo Dal Lago
- Crediti formativi: 6
- SSD: MAT/01
- Lingua di insegnamento: Italiano
- Moduli: Claudio Sacerdoti Coen (Modulo 1) Ugo Dal Lago (Modulo 2)
- Modalità didattica: Convenzionale - Lezioni in presenza (Modulo 1) Convenzionale - Lezioni in presenza (Modulo 2)
- Campus: Bologna
- Corso: Laurea Magistrale in Informatica (cod. 8028)
Conoscenze e abilità da conseguire
Al termine del corso, lo studente conosce le basi logico formali dell'informatica, in particolare, il lamb da calcolo e la sua teoria, corrispondenza tra programmi e dimostrazioni, il lamb da calcolo tipato semplice, i sistemi T ed F. È in grado di descrivere semplici funzioni numeriche in lamb da calcolo e di derivarne i tipi.
Contenuti
- La Logica nella Complessità Computazionale: Teoria dei Modelli Finiti, Teorema di Fagin, Teorema di Immerman-Vardi.
- La Logica nelle Basi di Dati: Algebra Relazionale, Calcolo Relazionale, Corrispondenza tra esse.
- La Logica nella Verifica di Sistemi: Strutture di Kripke, CTL*, CTL, LTL. Decidibilità del Problema del Model Checking.
Testi/Bibliografia
Joseph Y. Halpern, Robert Harper, Neil Immerman, Phokion G. Kolaitis, Moshe Y. Vardi, Victor Vianu. On the unusual effectiveness of logic in computer science. Bulletin of Symbolic Logic 7(2) pages 213--236. 2001.
Metodi didattici
Lezioni Frontali
Modalità di verifica e valutazione dell'apprendimento
Esame Orale.
Orario di ricevimento
Consulta il sito web di Ugo Dal Lago
Consulta il sito web di Claudio Sacerdoti Coen