IA 2

Corso di Intelligenza Artificiale 2 a.a. 2007/08

Docenti:
Giorgio Delzanno - tel. 6638 - email: giorgio <at> disi.unige.it
Maurizio Martelli - tel. 6727 - email: martelli <at> disi.unige.it

Scopo e temi del corso

Materiale per possibili seminari

Rappresentazione della Conoscenza, Ragionamento ed Apprendimento Automatico

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.

Programma

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

Logiche Costruttive (cenni)

Logica intuizionista

Logiche substrutturali: motivazioni e goal generali

Sintassi e sisteni deduttivi

Semantica alla Kripke

Logica multimodale

Esempi

conoscenza e credenze

logica deontica

logica dinamica

logica temporale

Procedure di decisione

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

Orario

Martedi e Mercoledi 9:30-11

Lezioni

25 Febbraio “conta degli studenti” e presentazione corso (1h)

28 Febbraio (delzanno) “Introduzione alla logica modale” (2h)

4 e 5 Marzo (delzanno) “semantica logica modale, logica multimodale, esempi, logica costruttiva” (4h)

11 e 12 Marzo (delzanno) “Logica LTL + LTL model checking” (4h)

18 e 19 Marzo (delzanno) “Esercizio LTL” (18 1 ora) e “Intro a CTL” (19)

26 marzo e 27 marzo “CTL model checking” (2h+2h)

1 aprile: “BDD-based model checking” (2h)

2 aprile: cancellata

15 Aprile (delzanno) “LTL e automi” (2h)

16 Aprile (martelli) “Introduzione ad automated deduction: risoluzione calcolo dei predicati, teorema Herbrand” (2h)

22 e 23 Aprile (delzanno) “LTL e automi” (22, 2h) “BMC” (23, 2h)

29 e 30 aprile (martelli) “continua”

Materiale per esame orale in linea

Riferimenti bibliografici (disponibili in biblioteca)

"Introduzione alla logica modale" (c'e' anche la nuova edizione "A new introduction to modal logic")
G. E. Hughes, M. J. Cresswell ; a cura di Claudio Pizzi

"Model Checking"
Edmund M. Clarke, Orna Grumberg and Doron A. Peled

"The temporal logic of reactive and concurrent systems"
Zohar Manna, Amir Pnueli

Logica simbolica (Tecniche Nuove, 1988)
C. Chang, R.C. Lee.

"Fondamenti di programmazione logica : i suoi rapporti con la logica e la matematica"
John W. Lloyd

"Handbook of logic in artificial intelligence and logic programming"
Dov. M. Gabbay

Dispense e note:

Dispense su Logiche Modali, Temporali e Model Checking (Delzanno) in formato ps

Lucidi su Theorem Proving (Martelli) in formato ppt

Dispense "Concepts, algorithms, and tools for model checking" (280 pagine) in formato ps
LTL, CTL, model checking, automi, Buchi automata, automata-based LTL model checking

Note su "LTL Model Checking" in formato gzipped-ps

Note su "Semantica di punto fisso per programmi logici" in formato PDF

Materiale sul web

Stanford Encyclopedia of Philosophy (SEP)

Logica e Intelligenza Artificiale

Logica modale

Logica temporale

Logica intuizionista

The logical foundations of cs (materiale on-line su logica modale, temporale, ecc)

Modalità d'esame

Seminario su argomento a scelta
(contattare via e-mail Giorgio Delzanno (giorgio <at> disi.unige.it) per la selezione dell'argomento)

Esame orale su argomenti visti a lezione (vedi materiale in linea)