Laurea specialistica in Informatica

Corso a esaurimento

Deduzione automatica (2008/2009)

Codice insegnamento 4S00050 Docente Maria Paola Bonacina crediti 5 Altri corsi di studio in cui è offerto Laurea specialistica in Sistemi intelligenti e multimediali Settore disciplinare INF/01 - INFORMATICA Lingua di erogazione Italiano Periodo 2° Q dal 26-gen-2009 al 27-mar-2009. Pagina Web http://profs.sci.univr.it/~bonacina/teachingUniVR/DA2008-09.html

Pagine collegate Avvisi relativi al corso Seminari relativi al corso

Orario lezioni

Obiettivi formativi

Il corso, insegnato in inglese, introduce problemi, metodi e sistemi del ragionamento automatico. La presentazione combina fondamenti teorici con questioni pratiche di natura algoritmico-implementativa, enfatizzando sistematicamente la meccanizzazione. Obbiettivo del corso è dare allo studente strumenti per progettare, applicare e valutare metodi e sistemi di ragionamento automatico, soprattutto per le applicazioni alla verifica automatica e semi-automatica di SW e HW. Pre-requisiti: conoscenze di logica ed algoritmi quali quelle impartite dai corsi dei primi tre anni.

Programma

Ragionamento automatico generale: procedure di prova come procedure di semi-decisione della validità o strategie di dimostrazione di teoremi. Strategia di dimostrazione di teoremi = sistema di inferenza + piano di ricerca. Il teorema di Herbrand. Strategie basate sugli ordinamenti ben fondati. Regole di inferenza di espansione: risoluzione, paramodulazione, sovrapposizione. Regole di inferenza di contrazione: sussunzione, riscrittura. Piani di ricerca. Ragionamento algoritmico: procedure di prova come procedure di decisione della soddisfacibilità. Teorie al prim'ordine e problemi decidibili in teorie al prim'ordine. Procedure di decisione e loro combinazione. Casi in cui le strategie di dimostrazione di teoremi sono procedure di decisione. Progetto e uso di ragionatori automatici.

Modalita d'esame

Esame mediante prove parziali:
vale solo per il primo appello dopo la fine delle lezioni, ovvero per la sessione di marzo-aprile, essendo il corso nel II quadrimestre. L'esame consta di un compito scritto (C) e di un progetto individuale (P) da realizzare a casa o in laboratorio durante il corso. 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ù.

Esame senza prove parziali:
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.

Note:
il compito scritto C (prova parziale) si tiene nella stessa data, ora e luogo dell'esame E della sessione di marzo-aprile (naturalmente contenuto e durata di C ed E saranno diversi).

Registrazione:
a ogni sessione la data dell'esame è la data dello scritto (E); per registrare il voto basta iscriversi allo scritto. Tutti i voti saranno registrati. Lo studente insoddisfatto di come sta andando l'esame puo' ritirarsi non consegnando C o E.

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

Valori relativi all'AA 2008/2009 calcolati su un campione di 47 iscritti. I valori in percentuale sono arrotondati al numero intero più vicino.