Acquisire la conoscenza della logica classica e di alcuni sistemi di logica non classica, della relativa semantica formale e metodi di dimostrazione. Acquisire la capacità di utilizzare le logiche studiate per la rappresentazione di realtà sia statiche che dinamiche. Presentazione di alcune importanti applicazioni della logica in ambito informatico
Curriculum
scheda docente materiale didattico
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).
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 Adottati
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).
Modalità Erogazione
Lezioni frontali ed esercitazioniModalità Valutazione
La verifica dell’apprendimento avviene attraverso una prova scritta della durata di circa 2 ore. Lo scritto è organizzato attraverso due o tre esercizi, finalizzati a verificare la comprensione dei concetti introdotti nel corso e la capacita` di utilizzarli per risolvere problemi semplici. I compiti di esame degli ultimi anni sono disponibili sul sito del corso: http://cialdea.dia.uniroma3.it/teaching/logica/. La valutazione in itinere e` costituita da 2 o 3 prove parziali che sostituiscono la prova finale. scheda docente materiale didattico
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).
Mutuazione: 20810263 Logica in Ingegneria informatica LM-32 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 Adottati
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).
Modalità Erogazione
Lezioni frontali ed esercitazioniModalità Valutazione
La verifica dell’apprendimento avviene attraverso una prova scritta della durata di circa 2 ore. Lo scritto è organizzato attraverso due o tre esercizi, finalizzati a verificare la comprensione dei concetti introdotti nel corso e la capacita` di utilizzarli per risolvere problemi semplici. I compiti di esame degli ultimi anni sono disponibili sul sito del corso: http://cialdea.dia.uniroma3.it/teaching/logica/. La valutazione in itinere e` costituita da 2 o 3 prove parziali che sostituiscono la prova finale.