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 |
---|---|---|
1° Q - 2° anno e successivi | 29-set-2003 | 28-nov-2003 |
2° Q | 12-gen-2004 | 12-mar-2004 |
3° Q | 5-apr-2004 | 11-giu-2004 |
Sessione | Dal | Al |
---|---|---|
Sessione straordinaria | 17-dic-2003 | 17-dic-2003 |
Sessione invernale | 17-mar-2004 | 17-mar-2004 |
Sessione estiva | 22-lug-2004 | 22-lug-2004 |
Sessione autunnale | 22-set-2004 | 22-set-2004 |
Periodo | Dal | Al |
---|---|---|
Festa di tutti i santi | 1-nov-2003 | 1-nov-2003 |
Vacanze natalizie | 22-dic-2003 | 6-gen-2004 |
Vacanze Pasquali | 8-apr-2004 | 13-apr-2004 |
Festa del Patrono S. Zeno | 12-apr-2004 | 12-apr-2004 |
Festa del lavoro | 1-mag-2004 | 1-mag-2004 |
Festa della Repubblica | 2-giu-2004 | 2-giu-2004 |
Vacanze estive | 26-lug-2004 | 31-ago-2004 |
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
Piano 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.
2° Anno Attivato nell'A.A. 2004/2005
Insegnamenti | Crediti | TAF | SSD |
---|
4° Anno Attivato nell'A.A. 2006/2007
Insegnamenti | Crediti | TAF | SSD |
---|
5° Anno Attivato nell'A.A. 2007/2008
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 (2006/2007)
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 8-gen-2007 al 9-mar-2007.
Sede
VERONA
Obiettivi formativi
Il corso assume conoscenze di logica ed algoritmi quali quelle impartite dai corsi dei primi tre anni, e presenta problemi, metodi e sistemi di ragionamento automatico, combinando fondamenti teorici con questioni pratiche di natura algoritmico-implementativa, in modo da preparare lo studente a progettare, valutare ed applicare metodi e sistemi di ragionamento automatico.
Programma
La nozione di procedura di prova come combinazione di sistema di inferenza e piano di ricerca; il teorema di Herbrand; strategie basate sulla generazione di istanze: dal metodo di Gilmore alla combinazione di hyperlinking con l'algoritmo di Davis-Putnam-Logemann-Loveland per SAT; strategie basate sugli ordinamenti ben fondati: schemi di inferenza di espansione (risoluzione, paramodulazione, sovrapposizione) e di contrazione (sussunzione, riscrittura) e piani di ricerca per il ragionamento in avanti; strategie basate sulla riduzione di goal: risoluzione lineare, tableaux, eliminazione di modelli e piani di ricerca per il ragionamento all'indietro; progetto e uso di dimostratori di teoremi; procedure di decisione; cenni alla costruzione di modelli; cenni alle applicazioni del ragionamento automatico alla verifica.
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 | Altro testo di riferimento |
Rolf Socher-Ambrosius, Patricia Johann | Deduction Systems (Edizione 1) | Springer Verlag | 1997 | 0387948473 | Testo adottato |
Klaus Truemper | Design of Logic-based Intelligent Systems (Edizione 1) | John Wiley and Sons | 2004 | 0471484032 | Altro testo di riferimento |
Raymond M. Smullyan | First-order logic | Dover Publications | 1995 | 0486683702 | Altro testo di riferimento |
Allan Ramsay | Formal Methods in Artificial Intelligence (Edizione 1) | Cambridge University Press | 1989 | 0521424216 | Altro testo di riferimento |
Chin-Liang Chang, Richard Char-Tung Lee | Symbolic Logic and Mechanical Theorem Proving (Edizione 1) | Academic Press | 1973 | 0121703509 | Testo adottato |
Alexander Leitsch | The Resolution Calculus (Edizione 1) | Springer | 1997 | 3540618821 | Altro testo di riferimento |
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 2007, 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 di programmazione (P) da realizzare a casa o in laboratorio durante il corso. Il lavoro di progetto comprende anche la
stesura di una breve relazione sul progetto (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 2007.
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. La data per la registrazione del voto sarà annunciata negli avvisi per studenti. Poichè i voti si registrano sul registro anche in assenza degli studenti, tutti i voti saranno registrati.
Tipologia di Attività formativa D e F
Documenti e avvisi
- Documento ufficiale (pdf, it, 21 KB, 25/06/03)
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.