CIALDEA MARTA
(programma)
Logica dei predicati classica (sintassi e semantica). Metodi di dimostrazione automatica. Il metodo di risoluzione. Raffinamenti della risoluzione e Risoluzione SLD. La programmazione logica e il linguaggio Prolog. Logiche modali e temporali. Il metodo dei tableaux per la logica temporale lineare. Applicazione alla verifica di sistemi.
(testi)
Vedi il sito del corso: http://cialdea.dia.uniroma3.it/teaching/logica/
M. Cialdea Mayer. Logica (dispense)
Qualsiasi testo di introduzione al Prolog.
Manuale utente di SWI-Prolog.
D. A. Peled. Software Reliability Methods. Springer, 2001 (capitoli 1 e 4).
M. Cialdea Mayer. Logica temporale e verifica di proprietà dei programmi (dispense).
|
Università Roma Tre