Deduzione automatica (2006/2007)

Corso a esaurimento

Codice insegnamento
4S00050
Docente
Maria Paola Bonacina
crediti
5
Altri corsi di studio in cui è offerto
Settore disciplinare
INF/01 - INFORMATICA
Lingua di erogazione
Italiano
Sede
VERONA
Periodo
2° Q dal 8-gen-2007 al 9-mar-2007.
Pagina Web
http://profs.sci.univr.it/~bonacina/teachingUniVR/DA2006-07.html

Orario lezioni

Obiettivi formativi

Il corso assume conoscenze di logica ed algoritmi quali quelle impartite dai corsi dei primi tre anni, e presenta problemi, metodi e sistemi di ragionamento automatico, combinando fondamenti teorici con questioni pratiche di natura algoritmico-implementativa, in modo da preparare lo studente a progettare, valutare ed applicare metodi e sistemi di ragionamento automatico.

Programma

La nozione di procedura di prova come combinazione di sistema di inferenza e piano di ricerca; il teorema di Herbrand; strategie basate sulla generazione di istanze: dal metodo di Gilmore alla combinazione di hyperlinking con l'algoritmo di Davis-Putnam-Logemann-Loveland per SAT; strategie basate sugli ordinamenti ben fondati: schemi di inferenza di espansione (risoluzione, paramodulazione, sovrapposizione) e di contrazione (sussunzione, riscrittura) e piani di ricerca per il ragionamento in avanti; strategie basate sulla riduzione di goal: risoluzione lineare, tableaux, eliminazione di modelli e piani di ricerca per il ragionamento all'indietro; progetto e uso di dimostratori di teoremi; procedure di decisione; cenni alla costruzione di modelli; cenni alle applicazioni del ragionamento automatico alla verifica.

Testi di riferimento
Autore Titolo Casa editrice Anno ISBN Note
Ricardo Caferra, Alexander Leitsch, Nicolas Peltier Automated Model Building (Edizione 1) Kluwer Academic Publishers 2004 1-4020-265 Altro testo di riferimento
Rolf Socher-Ambrosius, Patricia Johann Deduction Systems (Edizione 1) Springer Verlag 1997 0387948473 Testo adottato
Klaus Truemper Design of Logic-based Intelligent Systems (Edizione 1) John Wiley and Sons 2004 0471484032 Altro testo di riferimento
Raymond M. Smullyan First-order logic Dover Publications 1995 0486683702 Altro testo di riferimento
Allan Ramsay Formal Methods in Artificial Intelligence (Edizione 1) Cambridge University Press 1989 0521424216 Altro testo di riferimento
Chin-Liang Chang, Richard Char-Tung Lee Symbolic Logic and Mechanical Theorem Proving (Edizione 1) Academic Press 1973 0121703509 Testo adottato
Alexander Leitsch The Resolution Calculus (Edizione 1) Springer 1997 3540618821 Altro testo di riferimento

Modalità d'esame

Esame mediante prove parziali:
questa modalità vale solo per il primo appello dopo la fine delle lezioni, ovvero per la sessione di marzo-aprile 2007, essendo il corso nel II quadrimestre. In questa modalità, l'esame consta di un compito scritto di due ore (C) e di un progetto individuale di programmazione (P) da realizzare a casa o in laboratorio durante il corso. Il lavoro di progetto comprende anche la
stesura di una breve relazione sul progetto (max 4 pagine). Il voto d'esame è dato da: 50% C + 50% P.
Passato il primo appello dopo la fine delle lezioni, le prove parziali non valgono più nulla.
Chi sostiene l'esame mediante prove parziali deve iscriversi all'esame della sessione di marzo-aprile 2007.
Esame senza prove parziali:
in questa modalità, l'esame consta di un unico compito scritto (E), di difficoltà tale da uguagliare C + P, il cui voto determina il voto
d'esame. Questa modalità vale per tutti gli appelli. Tuttavia chi sostiene l'esame E al primo appello perde il voto maturato con 50% C + 50% P.
Note:
il compito scritto C (prova parziale) si
terrà nella stessa data, ora e luogo dell'esame E della sessione di marzo-aprile (naturalmente contenuto e durata di C ed E saranno diversi).
Il progetto P verrà consegnato via rete, eccetto la relazione che verrà consegnata quando si svolge il compito scritto C (prova parziale).
Registrazione:
a ogni sessione la data dell'esame è la data dello scritto (E); per registrare il voto basta iscriversi allo scritto. La data per la registrazione del voto sarà annunciata negli avvisi per studenti. Poichè i voti si registrano sul registro anche in assenza degli studenti, tutti i voti saranno registrati.

Condividi