LOGICA E SISTEMI INFORMATICI

Gli argomenti che seguono costituiscono il programma del corso di 9 CFU D.M.270/04.
Quelli contrassegnati con un asterisco sono relativi al solo esame integrativo di 4 CFU, Quelli contrassegnati con un asterisco o con un doppio asterisco al corso di Logica e Sistemi Informatici D.M. 509/99.

1. Logica proposizionale
   ([MC02] Cap. 1) Sintassi e semantica.
   Il calcolo di deduzione naturale.
   
2. Logica dei predicati
   ([MC02] Cap. 2, [IND], [SOL]) Sintassi e semantica.
   Il calcolo di deduzione naturale.
   Proprietà della logica dei predicati.
   Teorie del primo ordine.
   
3. Deduzione automatica
   ([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.
   
4. 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].
5. 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])
6. 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