Lo scopo del corso e' di approfondire ed ampliare gli aspetti di modellazione della conoscenza e ragionamento
automatico visti nel primo corso di intelligenza artificiale (basato sulla sola programmazione logica).

Utilizzando ancora linguaggi logici come supporto per la rappresentazione della conoscenza,  andremo ad
esplorare quali ulteriori (e forse piu naturali) linguaggi si possono utilizzare per modellare svariati aspetti
della realta: dalla modellazione di sistemi informatici alla  modellazione del comportamento umano.

Per tali linguaggi studieremo inoltre le tecniche utilizzate per lo sviluppo di procedure di decisione e ragionatori.

Infine, come integrazione alla parte di modellazione e ragionamento, vedremo un'altro aspetto
fondamentale dell'intelligenza artificiale: l'apprendimento automatico, cioe' una serie di tecniche
che consentono ad una macchina di apprendere nuove informazioni.

Il corso verra' concluso da una parte di seminari di argomenti selezionati dagli studenti.

Luigi Bozzo 1997s063@educ.disi.unige.it
Luca Chiarabini 1997s108@educ.disi.unige.it
Fabio Rossi 1997s022@educ.disi.unige.it
Andrea Olcese olcese@educ.disi.unige.it
Davide Roggero 1994s013@educ.disi.unige.it
Mirko Melis 1996s086@educ.disi.unige.it
Ombretta Pavarino 1996s022@educ.disi.unige.it

• Formato .ps.gz
• Formato .pdf

• Introduzione alla logica modale (Stanford Encyclopedia of Philosophy)
• The logical foundations of cs (materiale on-line su logica modale, temporale, ecc)
• Articolo del Dr. L. Van Der Torre relativo al seminario del 4 Aprile 2002 (From Deontic to Input Output Logic)

What is input output logic?  (per approfondimenti: pagina web L.Van Der Torre)
• Altro materiale su logica deontica
• Descrizione LTL e Algoritmi (Model Checking e SCC) (note in inglese)

• Seminario su argomento a scelta
• Presentazione di 10 minuti su uno degli argomenti del corso
• Esercizi su logica modale e temporale da svolgersi nell'arco di 10 giorni

Lezioni

Marzo
4-8  Martedi (2)-Venerdi (3): Deduzione Automatica (Martelli)
12 Martedi (2):  Deduzione Automatica (Martelli)
15 Venerdi (2): Esempi di modellazione tramite logica I ordine + Risoluzione
      Venerdi (1): Introduzione generale alla Logica Modale (Delzanno)

Vacanze Pasqua

Aprile
4 Aprile (2): Seminario Leon Van der Torre: Logica Deontica e Input Output
5 Aprile (2): Esercizi su logica modale (Delzanno)
 8: non ci sara' lezione
12 (1): Apprendimento (Martelli)
15-19: Logica Temporale  LTL  (Delzanno)
22-26: Procedure di Decisione per LTL e logica CTL  (Lu(2)-Ma(2)-Ve(2)) (Delzanno)
30 Aprile: Apprendimento (Martelli)
3 Maggio: CTL Model Checking
6-10 Maggio: Symbolic Model Checking (Delzanno)

Maggio
13-17:    Model checking e Planning  e Beliefs (Delzanno)
20-25: Seminari studenti/Seminario sull'uso di SAT (?)
27-31: Seminari studenti

• Luca Chiarabini: Logica Modale per il Calcolo degli Ambienti

Logica del prim'ordine

• Richiami di logica del prim'ordine
• Rappresentazione della conoscenza tramite logica del prim'ordine
• Ragionamento automatico
• Aspetti di base di theorem proving
• Metodi di risoluzione
• Teorema di Herbrand

• Logica intuizionista
• Logiche substrutturali: motivazioni e goal generali

Nota: possile integrazione con seminari su sintassi/semantica

• Sintassi e sisteni deduttivi
• Semantica alla Kripke
• Logica multimodale
• Esempi
• conoscenza e credenze
• logica deontica
• logica dinamica
• logica temporale

• Model Checking
• Logica Temporale CTL e LTL
• Esempi di sistemi e proprieta'
• Algoritmi di model checking

 
• Symbolic Model Checking:
• Strutture dati efficienti (BDDs)
• Algoritmi simbolici
• Constraints per sistemi infiniti

 
• Applicazioni di Model checking
• verifica di sistemi
• planning

• Decision trees
• Inductive Logic Programming