Obiettivi formativi

Il corso presenta problemi, metodi e sistemi del ragionamento automatico, combinando fondamenti teorici con questioni pratiche di natura algoritmico-implementativa. L'obbiettivo del corso è dare allo studente strumenti per progettare, applicare e valutare metodi e sistemi di ragionamento automatico. Il corso prepara per una tesi di Laurea Specialistica o Magistrale nell'area del ragionamento automatico. 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.

Modalità d'esame

Esame mediante prove parziali:
questa modalità vale solo per il primo appello dopo la fine delle lezioni, ovvero per la sessione di marzo-aprile, essendo il corso nel II quadrimestre. In questa modalità, l'esame consta di un compito scritto di due ore (C) e di un progetto individuale (P) da realizzare a casa o in laboratorio durante il corso. Il lavoro di progetto comprende la stesura di una breve relazione (max 4 pagine). 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ù nulla. Chi sostiene l'esame mediante prove parziali deve iscriversi all'esame della sessione di marzo-aprile.

Esame senza prove parziali:
in questa modalità, 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. Tuttavia chi sostiene l'esame E al primo appello perde il voto maturato con 50% C + 50% P.

Note:
il compito scritto C (prova parziale) si
terrà nella stessa data, ora e luogo dell'esame E della sessione di marzo-aprile (naturalmente contenuto e durata di C ed E saranno diversi).
Il progetto P verrà consegnato via rete, eccetto la relazione che verrà consegnata quando si svolge il compito scritto C (prova parziale).

Registrazione:
a ogni sessione la data dell'esame è la data dello scritto (E); per registrare il voto basta iscriversi allo scritto. Non è previsto il rifiuto del voto e tutti i voti saranno registrati. Lo studente insoddisfatto di come sta andando l'esame può ritirarsi: per ritirarsi è sufficiente non consegnare C o E.