30214 - FONDAMENTI LOGICI DELL'INFORMATICA

Scheda insegnamento

Anno Accademico 2018/2019

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.

Programma/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 dell'apprendimento

Esame Orale.

Orario di ricevimento

Consulta il sito web di Ugo Dal Lago

Consulta il sito web di Claudio Sacerdoti Coen