Deduzione automatica (2004/2005)

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
Periodo
2° Q dal 10-gen-2005 al 11-mar-2005.
Pagina Web
http://profs.sci.univr.it/~bonacina/teachingUniVR/DA.html

Orario lezioni

2° Q
Giorno Ora Tipo Luogo Note
lunedì 16.30 - 18.30 lezione Aula C  
martedì 8.30 - 9.30 lezione Aula C  
mercoledì 16.30 - 18.30 lezione Aula A  

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; 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 goals: risoluzione lineare, tableaux, eliminazione di modelli e piani di ricerca per il ragionamento all'indietro; progetto e uso di dimostratori di teoremi; cenni di costruzione di modelli; cenni sulle applicazioni del ragionamento automatico alla matematica e alla verifica.

Testi di riferimento
Autore Titolo Casa editrice Anno ISBN Note
Rolf Socher-Ambrosius, Patricia Johann Deduction Systems (Edizione 1) Springer Verlag 1997 0387948473 Libro di testo adottato dal corso
Klaus Truemper Design of Logic-based Intelligent Systems (Edizione 1) John Wiley and Sons 2004 0471484032 Consigliato per consultazione oltre ai libri adottati
Raymond M. Smullyan First-order logic Dover Publications 1995 0486683702 Consigliato per consultazione oltre ai libri adottati
Allan Ramsay Formal Methods in Artificial Intelligence (Edizione 1) Cambridge University Press 1989 0521424216 Consigliato per consultazione oltre ai libri adottati
Chin-Liang Chang, Richard Char-Tung Lee Symbolic Logic and Mechanical Theorem Proving (Edizione 1) Academic Press 1973 0121703509 Libro di testo adottato dal corso
Alexander Leitsch The Resolution Calculus (Edizione 1) Springer 1997 3540618821 Consigliato per consultazione oltre ai libri adottati

Modalità d'esame

per l'esame lo studente svolge un progetto e lo presenta in forma sia scritta che orale. Lo studente può scegliere tra un progetto pratico e un progetto teorico. Una lista di progetti tra cui scegliere sarà presentata a lezione. Un progetto pratico consiste nello studiare ed usare un sistema di ragionamento automatico (e.g., dimostratore di teoremi) allo stato dell'arte. Un progetto teorico consiste nello studiare un soggetto teorico non trattato a lezione. In entrambi i casi il progetto applica ed estende gli argomenti trattati nel corso. Lo studente che sceglie il progetto pratico dovrà scaricare il sistema dal suo sito web, compilarlo, imparare ad usarlo, ovvero capire come presentare un problema in ingresso e come interpretare il risultato in uscita, e valutarlo empiricamente. Per far questo studierà il manuale del sistema ed articoli apparsi in letteratura sul sistema stesso. Lo studente che sceglie il progetto teorico dovrà studiare una collezione di articoli sull'argomento. In entrambi i casi lo studente dovrà preparare una breve relazione scritta e dare una presentazione orale del suo soggetto. Il voto d'esame sarà determinato al 50% dalla relazione scritta e al 50% dalla presentazione orale.

Materiale didattico

Documenti

Statistiche per i requisiti di trasparenza (Attuazione Art. 2 del D.M. 31/10/2007, n. 544)

Statistiche esiti
Esiti Esami Esiti Percentuali Media voti Deviazione Standard
Positivi 100.0% 28 2
Respinti --
Assenti --
Ritirati --
Annullati --
Distribuzione degli esiti positivi
18 19 20 21 22 23 24 25 26 27 28 29 30 30 e Lode
0.0% 0.0% 0.0% 0.0% 0.0% 0.0% 0.0% 33.3% 0.0% 0.0% 0.0% 33.3% 33.3% 0.0%

Valori relativi all'AA 2004/2005 calcolati su un totale di 3 iscritti. I valori in percentuale sono arrotondati al numero intero più vicino.