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.
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.
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 |
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.