Ragionamento automatico (2013/2014)

Codice insegnamento
4S02796
Docente
Maria Paola Bonacina
Coordinatore
Maria Paola Bonacina
crediti
6
Settore disciplinare
INF/01 - INFORMATICA
Lingua di erogazione
Italiano
Periodo
I semestre dal 1-ott-2013 al 31-gen-2014.
Pagina Web
http://profs.sci.univr.it/~bonacina/teachingUniVR/RA.html

Orario lezioni

I semestre
Giorno Ora Tipo Luogo Note
lunedì 11.30 - 13.30 lezione Aula G  
giovedì 14.30 - 16.30 lezione Aula C  

Obiettivi formativi

Il corso introduce problemi, metodi e sistemi del ragionamento automatico. La presentazione combina fondamenti teorici con questioni pratiche di natura algoritmico-implementativa, con enfasi sulla meccanizzazione. Obiettivo del corso è dare allo studente strumenti per progettare, applicare e valutare metodi e sistemi di ragionamento automatico, per applicazioni in analisi, verifica e sintesi di sistemi, ed in intelligenza artificiale.

Programma

Fondamenti del ragionamento automatico: dimostrazione di teoremi e costruzione di modelli. Sistemi di inferenza, quali: per generazione di istanze (e.g., hyper-linking), basati su ordinamenti (e.g., per completamento), e basati su riduzione di sotto-goal (e.g., eliminazione di modelli). Piani di ricerca. Ragionamento algoritmico in ambiti specifici, quali: procedure di decisione per soddisfacibilità modulo teorie (SMT); ragionamento su vincoli. Progetto e uso di ragionatori generici o specifici.

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
Daniel Kroening, Ofer Strichman Decision Procedures. An algorithmic point of view Springer 2008 978-3-540-74104-6
Chin-Liang Chang, Richard Char-Tung Lee Symbolic Logic and Mechanical Theorem Proving (Edizione 1) Academic Press 1973 0121703509
Alexander Leitsch The Resolution Calculus (Edizione 1) Springer 1997 3540618821
Martin Davis The Universal Computer. The Road from Leibniz to Turing. Turing Centenary Edition. Taylor and Francis Group 2012 978-1-4665-0519-3

Modalità d'esame

Esame mediante prove parziali:
Il voto è dato da 30% C1 + 30% C2 + 40% P, dove C1 è la prova intermedia, C2 è la prova finale, e P è un progetto. Il voto così generato viene registrato al I appello della sessione di febbraio.
Esame senza prove parziali:
Il voto è dato da 100% E, dove E è un unico compito scritto, di difficoltà tale da uguagliare l'unione delle prove parziali.
Registrazione: non è previsto il rifiuto del voto e tutti i voti saranno registrati. Lo studente può ritirarsi informando la docente.
Tutti gli elaborati sono individuali. È vietato copiare o condividere codice o testo e le copiature determineranno abbassamenti di voti.

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 100.0% 20 0
Respinti --
Assenti --
Ritirati --
Annullati --
Distribuzione degli esiti positivi
18 19 20 21 22 23 24 25 26 27 28 29 30 30 e Lode
0.0% 0.0% 100.0% 0.0% 0.0% 0.0% 0.0% 0.0% 0.0% 0.0% 0.0% 0.0% 0.0% 0.0%

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