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
Sede
VERONA
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

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.

Condividi