Programma del corso e materiale di riferimento (fino all'a.a. 2014/15)

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. 1 di MC02, o dal Cap. 2 delle dispense MC14.

Argomenti del corso

1. Logica dei predicati ([MC14], oppure:
   [MC02] Cap. 2, [IND] ) Sintassi e semantica.
   Il calcolo di deduzione naturale.
   Proprietà della logica dei predicati.
   Teorie del primo ordine.
   
2. Deduzione automatica ([MC14], oppure: [MC02] Cap. 3, escluso paragrafo 3.5) 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.
   
3. Il linguaggio Prolog (Qualunque testo di introduzione al Prolog, ad esempio [Bra88], [CM93] [CLMM97].
   I testi seguenti contengono materiale più avanzato sul linguaggio Prolog: [NM95], [Sho94].) Il compilatore utilizzato è SWI-Prolog [SWI].
4. Il calcolo delle situazioni e il linguaggio GOLOG ([MC11], [GOLOG].
   Consultare anche: [Rei01]: Capitoli 3 (esclusi paragrafi 3.2.1, 3.2.2, 3.2.6),
   6 (esclusi paragrafi 6.3.2 e 6.5)
   e 10 (soltanto i paragrafi 10.1, 10.2 e 10.5, e gli esercizi del paragrafo 10.8 ad essi collegati);
   e: [LRLLS])
5. Metodi formali per la verifica di sistemi ([Pel01] capitoli 1-6, [MC09].) Modellazione di un sistema (sistemi di transizioni)
   Linguaggi di specifica formale: logica temporale lineare
   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
   

Materiale di riferimento

• [MC14] M. Cialdea Mayer. Logica (dispense, che contengono il materiale necessario per il corso estratto da [MC02], con integrazioni derivanti da [IND] e soluzione di alcuni esercizi).

• [MC02] M. Cialdea Mayer. Logica. Linguaggio, ragionamento, calcolo. Esculapio, 2002.

• [IND] Indecidibilità della logica dei predicati (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.

• [CLMM97] L. Console, E. Lamma, P. Mello, M. Milano. Programmazione Logica e Prolog. UTET Libreria, 1997.

• [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)

• [MC11] Il Calcolo delle Situazioni e il linguaggio Golog (dispense).

• [GOLOG] Il linguaggio Golog

• [Rei01] R. Reiter. Knowledge in Action: Logical Foundations for Specifying and Implementing Dynamical Systems. MIT Press, 2001. (Presente in Biblioteca Scientifico-tecnologica, sede centrale, collocazione 006.332 REI-K 2001.)
  Il codice GOLOG presentato nel libro si può trovare sul sito stesso del libro.

• [LRLLS] H.J. Levesque, R. Reiter, Y. Lespérance, F. Lin, R.B. Scherl. GOLOG: A Logic Programming Language for Dynamic Domains. Journal of Logic Programming, 31, 1997, 59-84. (A questa ed altre pubblicazioni su GOLOG si può accedere dal sito del Gruppo di Robotica Cognitiva dell'Università di Toronto.)

• [Pel01] D. A. Peled. Software Reliability Methods. Springer, 2001. (Presente in Biblioteca Scientifico-tecnologica, sede centrale, collocazioni 005.14 PEL-S 2001 e 005.14 PEL-S 2001a.)
  Gli argomenti dei capitoli 5 e 6 di questo testo sono trattati anche nelle dispense MC09. Per l'introduzione ai metodi formali e la modellazione di sistemi il libro di Peled resta l'unico riferimento (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).