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.
Calendario accademico
Il calendario accademico riporta le scadenze, gli adempimenti e i periodi rilevanti per la componente studentesca, personale docente e personale dell'Università. Sono inoltre indicate le festività e le chiusure ufficiali dell'Ateneo.
L’anno accademico inizia il 1° ottobre e termina il 30 settembre dell'anno successivo.
Calendario didattico
Il calendario didattico indica i periodi di svolgimento delle attività formative, di sessioni d'esami, di laurea e di chiusura per le festività.
Periodo | Dal | Al |
---|---|---|
Periodo zero | 19-set-2005 | 10-ott-2005 |
1° Q - 2° anno e successivi | 3-ott-2005 | 2-dic-2005 |
1° Q - 1° Anno | 17-ott-2005 | 2-dic-2005 |
2° Q | 8-gen-2006 | 9-mar-2006 |
3° Q | 3-apr-2006 | 9-giu-2006 |
Sessione | Dal | Al |
---|---|---|
Esami periodo 0 | 17-ott-2005 | 21-ott-2005 |
I Sessione esami | 12-dic-2005 | 23-dic-2005 |
II Sessione esami | 20-mar-2006 | 31-mar-2006 |
Sessione estiva | 19-giu-2006 | 28-lug-2006 |
Sessione autunnale | 4-set-2006 | 29-set-2006 |
Sessione | Dal | Al |
---|---|---|
Sessione straordinaria | 14-dic-2005 | 14-dic-2005 |
Sessione invernale | 15-mar-2006 | 15-mar-2006 |
Sessione estiva | 19-lug-2006 | 19-lug-2006 |
Sessione autunnale | 13-set-2006 | 13-set-2006 |
Periodo | Dal | Al |
---|---|---|
Festa di tutti i Santi | 1-nov-2005 | 1-nov-2005 |
Immacolata Concezione | 8-dic-2005 | 8-dic-2005 |
Vacanze Natalizie | 23-dic-2005 | 7-gen-2006 |
Vacanze Pasquali | 13-apr-2006 | 19-apr-2006 |
Festa della Liberazione | 25-apr-2006 | 25-apr-2006 |
Festa dei Lavoratori | 1-mag-2006 | 1-mag-2006 |
Festività Santo Patrono | 21-mag-2006 | 21-mag-2006 |
Festa della Repubblica | 2-giu-2006 | 2-giu-2006 |
Vacanze Estive | 31-lug-2006 | 31-ago-2006 |
Calendario esami
Gli appelli d'esame sono gestiti dalla Unità Operativa Segreteria Corsi di Studio Scienze e Ingegneria.
Per consultazione e iscrizione agli appelli d'esame visita il sistema ESSE3.
Per problemi inerenti allo smarrimento della password di accesso ai servizi on-line si prega di rivolgersi al supporto informatico della Scuola o al servizio recupero credenziali
Docenti
Squassina Marco
marco.squassina@univr.it +39 045 802 7913Piano Didattico
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.
3° Anno Attivato nell'A.A. 2007/2008
Insegnamenti | Crediti | TAF | SSD |
---|
4° Anno Attivato nell'A.A. 2008/2009
Insegnamenti | Crediti | TAF | SSD |
---|
5° Anno Attivato nell'A.A. 2009/2010
Insegnamenti | Crediti | TAF | SSD |
---|
Insegnamenti | Crediti | TAF | SSD |
---|
Insegnamenti | Crediti | TAF | SSD |
---|
Insegnamenti | Crediti | TAF | SSD |
---|
Insegnamenti | Crediti | TAF | SSD |
---|
Insegnamenti | Crediti | TAF | SSD |
---|
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.
Deduzione automatica (2008/2009)
Codice insegnamento
4S00050
Docente
Crediti
5
Offerto anche nei corsi:
- Deduzione automatica del corso Laurea specialistica in Sistemi intelligenti e multimediali
Lingua di erogazione
Italiano
Settore Scientifico Disciplinare (SSD)
INF/01 - INFORMATICA
Periodo
2° Q dal 26-gen-2009 al 27-mar-2009.
Sede
VERONA
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.
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.
Tipologia di Attività formativa D e F
Insegnamenti non ancora inseriti
Prospettive
Avvisi degli insegnamenti e del corso di studio
Per la comunità studentesca
Se sei già iscritta/o a un corso di studio, puoi consultare tutti gli avvisi relativi al tuo corso di studi nella tua area riservata MyUnivr.
In questo portale potrai visualizzare informazioni, risorse e servizi utili che riguardano la tua carriera universitaria (libretto online, gestione della carriera Esse3, corsi e-learning, email istituzionale, modulistica di segreteria, procedure amministrative, ecc.).
Entra in MyUnivr con le tue credenziali GIA: solo così potrai ricevere notifica di tutti gli avvisi dei tuoi docenti e della tua segreteria via mail e a breve anche tramite l'app Univr.