Programma del corso e materiale di riferimento
Il programma del corso di Logica per l'Informatica
degli anni accademici precedenti si può trovare
qui.
Prerequisiti
Il corso presuppone la conoscenza dei concetti fondamentali
alla base della sintassi e semantica della
logica proposizionale (o booleana), quali è
possibile acquisire
dal Cap. 2 delle dispense MC14.
Argomenti del corso
- Logica dei predicati
([MC14])
Sintassi e semantica.
Proprietà della logica dei predicati.
Teorie del primo ordine.
- Deduzione automatica
([MC14])
Il metodo dei tableaux per la logica proposizionale.
Algoritmo di unificazione.
Il metodo di risoluzione.
Raffinamenti della risoluzione: risoluzione lineare, risoluzione
con clausole unitarie.
Risoluzione SLD e programmazione logica.
- Cenni sul linguaggio Prolog
(Qualunque testo di introduzione al Prolog, ad esempio
[Bra88],
[CM93],
[CLMM97],
[FL88].
Per chi è interessato, i
testi seguenti contengono materiale più avanzato sul
linguaggio Prolog:
[NM95],
[Sho94].)
Il compilatore utilizzato è SWI-Prolog
[SWI].
- Metodi formali per la verifica di sistemi
([Pel] capitoli 1-6,
[MC09])
Modellazione di un sistema (sistemi di transizioni).
Linguaggi di specifica formale: logica temporale lineare (LTL).
Tableaux per la logica temporale lineare.
Automi su parole infinite, automi di Büchi.
Traduzione di formule LTL in automi.
Verifica di proprietà di un sistema rappresentate da formule
LTL.
Cenni sul tool per la verifica formale di sistemi software
SPIN.
Materiale di riferimento
-
[MC14]
M. Cialdea Mayer.
Logica (dispense)
-
[Bra88]
I. Bratko.
Programmare in Prolog per l'Intelligenza Artificiale.
Masson - Addison Wesley, 1988.
-
[CM93]
W. F. Clocksin and C. S. Mellish.
Programmare in Prolog.
Franco Angeli, 1993.
(Il testo originale, in inglese, è disponibile
online)
-
[CLMM97]
L. Console, E. Lamma, P. Mello, M. Milano.
Programmazione Logica
e Prolog.
UTET Libreria, 1997.
-
[FL88]
F. Furlan e G.A. Lanzarone.
Prolog. Linguaggio e metodologia di programmazione logica.
Franco Angeli, 1988. Il libro è fuori stampa, ma si può
scaricare la
versione pdf.
-
[NM95]
U. Nilsson and J. Maluszynski.
Logic, Programming and Prolog.
John Wiley & Sons, 1995.
-
[Sho94]
Y. Shoham.
Artificial Intelligence techniques in Prolog.Morgan Kaufmann, 1994.
-
[SWI]
SWI-Prolog: un compilatore Prolog (Free Software).
Ambienti e strumenti di programmazione:
Program development tools
SWI prolog editor (segnalato da uno studente, non testato dal docente)
Per chi lavora in ambiente
emacs o
Xemacs:
Prolog mode per Emacs (per sistemi Linux Debian o Ubuntu,
istallare il pacchetto prolog-el)
-
[Pel]
D. A. Peled.
Software Reliability Methods.
Springer, 2001.
Gli argomenti dei
capitoli 5 e 6 di questo testo sono trattati anche nelle dispense
MC09.
Questo testo è utile soprattutto per l'introduzione ai metodi
formali e la modellazione di sistemi (capitoli 1 e 4). Si noti che i
capitoli 2 e 3 dello stesso testo riguardano concetti di base trattati
in altra parte del corso.
-
[MC09]
M. Cialdea Mayer.
Logica temporale e verifica di proprietà dei programmi (dispense).
