Studiare

In questa sezione è possibile reperire le informazioni riguardanti l'organizzazione pratica del corso, lo svolgimento delle attività didattiche, le opportunità formative e i contatti utili durante tutto il percorso di studi, fino al conseguimento del titolo finale.

Piano Didattico

A.A. 2024/2025 A.A. 2023/2024 A.A. 2022/2023 A.A. 2021/2022 A.A. 2020/2021 A.A. 2019/2020 A.A. 2018/2019 A.A. 2017/2018 A.A. 2016/2017 A.A. 2015/2016 A.A. 2014/2015 A.A. 2013/2014 A.A. 2012/2013 A.A. 2011/2012 A.A. 2010/2011 A.A. 2009/2010

Queste informazioni sono destinate esclusivamente agli studenti e alle studentesse già iscritti a questo corso.
Se sei un nuovo studente interessato all'immatricolazione, trovi le informazioni sul percorso di studi alla pagina del corso:

Laurea magistrale in Ingegneria e scienze informatiche - Immatricolazione dal 2025/2026

Il piano didattico è l'elenco degli insegnamenti e delle altre attività formative che devono essere sostenute nel corso della propria carriera universitaria.
Selezionare il piano didattico in base all'anno accademico di iscrizione.

CURRICULUM TIPO:

1° Anno 

InsegnamentiCreditiTAFSSD
12
B
ING-INF/05
12
B
INF/01
6
B
ING-INF/05
6
B
ING-INF/05
12
B
ING-INF/05
6
B
ING-INF/05

2° Anno   Attivato nell'A.A. 2014/2015

InsegnamentiCreditiTAFSSD
6
B
ING-INF/05
6
B
INF/01
Altre attivita' formative
4
F
-
24
E
-
InsegnamentiCreditiTAFSSD
12
B
ING-INF/05
12
B
INF/01
6
B
ING-INF/05
6
B
ING-INF/05
12
B
ING-INF/05
6
B
ING-INF/05
Attivato nell'A.A. 2014/2015
InsegnamentiCreditiTAFSSD
6
B
ING-INF/05
6
B
INF/01
Altre attivita' formative
4
F
-
24
E
-
Insegnamenti Crediti TAF SSD
Tra gli anni: 1°- 2°
Tre insegnamenti a scelta tra i seguenti
6
C
INF/01
6
C
INF/01
6
C
FIS/01
6
C
INF/01
6
C
INF/01
6
C
INF/01
6
C
INF/01
6
C
SECS-P/10
6
C
INF/01
6
C
INF/01
6
C
INF/01
6
C
INF/01
6
C
INF/01
6
C
INF/01
6
C
INF/01
6
C
INF/01
Tra gli anni: 1°- 2°
8
D
-

Legenda | Tipo Attività Formativa (TAF)

TAF (Tipologia Attività Formativa) Tutti gli insegnamenti e le attività sono classificate in diversi tipi di attività formativa, indicati da una lettera.

A Attività di base
B Attività caratterizzanti
C Attività formative affini o integrative
D Attività a scelta dello studente
E Prova finale
F Altre attività formative
S Stage e tirocini presso imprese, enti pubblici o privati, ordini professionali

Ragionamento automatico  (2014/2015)

Codice insegnamento

4S02796

Docente

Maria Paola Bonacina

Coordinatore

Maria Paola Bonacina

Crediti

6

Lingua di erogazione

Italiano

Settore Scientifico Disciplinare (SSD)

INF/01 - INFORMATICA

Periodo

I sem. dal 1 ott 2014 al 30 gen 2015.

Pagina Web

http://www.di.univr.it/?ent=oi&aa=2014%2F2015&codiceCs=S71&codins=4S02796&cs=417&discr=&discrCd=&lang=it

Seminari 0

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, sintesi di sistemi, e 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., risoluzione), 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 Lettura supplementare
Daniel Kroening, Ofer Strichman Decision Procedures. An algorithmic point of view Springer 2008 978-3-540-74104-6 Libro di testo
Rolf Socher-Ambrosius, Patricia Johann Deduction Systems (Edizione 1) Springer Verlag 1997 0387948473 Lettura supplementare
Raymond M. Smullyan First-order logic Dover Publications 1995 0486683702 Lettura supplementare
Allan Ramsay Formal Methods in Artificial Intelligence (Edizione 1) Cambridge University Press 1989 0521424216 Lettura supplementare
Chin-Liang Chang, Richard Char-Tung Lee Symbolic Logic and Mechanical Theorem Proving (Edizione 1) Academic Press 1973 0121703509 Libro di testo
Alexander Leitsch The Resolution Calculus (Edizione 1) Springer 1997 3540618821 Lettura supplementare
Martin Davis The Universal Computer. The Road from Leibniz to Turing. Turing Centenary Edition. Taylor and Francis Group 2012 978-1-4665-0519-3 Lettura supplementare

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.

Le/gli studentesse/studenti con disabilità o disturbi specifici di apprendimento (DSA), che intendano richiedere l'adattamento della prova d'esame, devono seguire le indicazioni riportate QUI