Deduzione automatica (2008/2009)

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 26-gen-2009 al 27-mar-2009.
Pagina Web
http://profs.sci.univr.it/~bonacina/teachingUniVR/DA2008-09.html

Orario lezioni

2° Q
Giorno Ora Tipo Luogo Note
martedì 12.30 - 13.30 lezione Aula D  
mercoledì 14.30 - 16.30 lezione Aula F dal 11-feb-2009  al 27-mar-2009
venerdì 11.30 - 13.30 lezione Aula D  

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.

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 Testo supplementare
Rolf Socher-Ambrosius, Patricia Johann Deduction Systems (Edizione 1) Springer Verlag 1997 0387948473 Testo adottato
Chin-Liang Chang, Richard Char-Tung Lee Symbolic Logic and Mechanical Theorem Proving (Edizione 1) Academic Press 1973 0121703509 Testo adottato
Aaron R. Bradley, Zohar Manna The Calculus of Computation - Decision Procedures with Applications to Verification (Edizione 1) Springer 2007 9783540741 Testo adottato
Alexander Leitsch The Resolution Calculus (Edizione 1) Springer 1997 3540618821 Testo supplementare

Modalità 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)

Statistiche esiti
Esiti Esami Esiti Percentuali Media voti Deviazione Standard
Positivi 61.70% 25 4
Respinti 8.51%
Assenti 21.27%
Ritirati 8.51%
Annullati --
Distribuzione degli esiti positivi
18 19 20 21 22 23 24 25 26 27 28 29 30 30 e Lode
10.3% 0.0% 20.6% 0.0% 10.3% 3.4% 0.0% 0.0% 0.0% 17.2% 6.8% 10.3% 13.7% 6.8%

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