Logiche per Informatica
Docente: Prof. Nicola Olivetti
Programma del Corso per l'a.a. 2003-04
PARTE 0 Logica Proposizionale Classica (LPC)
- Calcolo proposizionale classico, assiomatizzazione, correttezza e
completezza
- Metodo di prova a Tableaux per LPC
PARTE I Logiche Modali
- Il linguaggio delle Logiche Modali, differenti
Interpretazione della Modalità
- Semantica dei Modelli di Kripke
- Sistemi assiomatici per K e le sue estensioni principali, correttezza e
completezza
- Metodo di prova a Tableaux per logiche modali, correttezza e
completezza
PARTE II Logiche modali per la conoscenza
- Logiche multimodali con interpretazione epistemica, nozione di Common
Knowledge
- I giochi dei Three Wise Men e dei Muddy Children
- Conoscenza comune nei sistemi distribuiti, il problema dell'Attacco
Coordinato
PARTE III Logiche temporali per sistemi concorrenti/distribuiti
(A) Logica del tempo lineare (LTL)
- Sintassi, semantica modale, assiomatizzazione, esempi di proprieta', forme
normali
- Model checking di proprieta' mediante automi: Automi di Büchi
- Traduzione di una formula LTL in un automa di Büchi generalizzato
- Equivalenza tra automi generalizzati e automi comuni
- Prodotto di Automi
(B) Logica temporale del tempo ramificato (CTL)
- Sintassi e semantica, esempi di proprietà
- Algoritmo di Model Checking per CTL
PARTE IV Logica Intuizionista
- Motivazioni, formalizzazione del ragionamento costruttivo, il linguaggio
della logica intuizionista
- Calcolo della Deduzione Naturale per la logica intuizionista (e per la
logica classica)
- Assiomatizzazione della logica intuizionista e sua equivalenza con la
Deduzione Naturale
- Semantica di Kripke per la logica intuizionista, correttezza e completezza
dell'assiomatizzazione
- Relazione tra logica classica LPC e logica intuizionista, Teorema di
Glivenko
- Relazione tra logica intuizionista e logiche modali (interpretazione in
S4)
PARTE V Logiche Terminologiche (Descriprion Logics)
- Il linguaggio ALCN, sintassi e semantica
- Equivalenza di ALC e della logica K-multimodale
- Strutturazione di basi di conoscenza terminologiche: TBOX e ABOX, TBOX
definitorie e cicliche
- Inferenze riguardanti TBOX (sussunzione di concetti, consistenza etc.) e
ABOX
- Metodo di prova a Tableaux per ALCN
- Il linguaggio OIL per il Web semantico e la sua corrispondenza con le
Description logics.
Modalità di esame per l'anno corrente: discussione degli esercizi
assegnati
Esercizi Assegnati
Testi di riferimento/approfondimento
L'indicazione (D) significa che il testo è reperibile attualmente in
Biblioteca.
Logica in generale:
G. Lolli. Introduzione alla logica formale. Il Mulino, 1991.
(D)
Logiche Modali:
- M. Fitting. Proof methods for modal and intuitionistic logics, D. Reidel,
1983. (D)
- M.G. E. Hughes, M. J. Crewell. A new introduction to modal logic.
Routledge, 1996, (D)
Logiche per la conoscenza, conoscenza comune:
- M. Huth, M. Ryan. Logic in Computer Science: Modeling and reasoning about
systems. Cambridge University Press, 2000.
- J. Halpern and Y. Moses. Knowledge and common knowledge in a distributed
environment. Journal of the ACM, 37(3):549--587, 1990. (D)
- J Meyer and W. van der Hoek, Epistemic Logic for AI and Computer Science,
Cambridge Tracts in Theoretical Computer Science, vol. 41, Cambridge
University Press, 1995. (D)
Logiche temporali:
- Jost-Pieter Katoen: "Concepts algorithms and tools for model checking",
lecture notes disponibili al sito
http://www.diku.dk/topps/activities/model/
(D)
- D. Peled
. Software Reliability
Methods, Springer-Verlag, 2001. (D)
- M. Huth, M. Ryan. Logic in Computer Science: Modeling and reasoning about
systems. Cambridge University Press, 2000.
Logica intuizionista:
- Dirk van Dalen, Intuitionistic Logic, in:Gabbay, D. M.(ed.) Handbooks of
Philosophical Logic, Vol.III, P. Reidel, pp. 225-339, 1986. (D)
Description Logics:
- F. Baader, D. Calvanese, D. McGuiness, D. Nardi, and P. Patel-Schneider,
editors. The Description Logic Handbook -Theory, Implementation and
Applications. Cambridge University Press, 2003.
.