Orario di ricevimento: ogni giovedì alle 11:00, salvo avvisi contrari comunicati sul newsgroup.
È stato creato il newsgroup unibo.cs.informatica.linguaggi per mantenere il contatto fra gli studenti e con il docente.
Il corso prevede delle attività da svolgersi in laboratorio utilizzando il dimostratore interattivo di teoremi Matita. Lo studente ha a disposizione due ore per svolgere in laboratorio gli esercizi assegnati loro. Al termine delle due ore avviene la consegna con relativa valutazione. Successivamente lo studente ha a disposizione una settimana per completare o correggere gli esercizi svolti per migliorare il punteggio ottenuto.
I punteggi conseguiti nelle prove di laboratorio concorrono al voto finale. Gli studenti che non prendono parte all'attività in laboratorio debbono sostenere un orale integrativo obbligatorio.
Oltre all'attività in laboratorio e all'eventuale orale integrativo, per superare la parte di Linguaggi è inoltre necessario superare un esame scritto. L'esame scritto si compone di due parti. La prima parte durante, la quale non e' possibile utilizzare appunti, comprende domande di teoria (enunciare definizioni, teoremi, dimostrare semplici teoremi, dimostrare teoremi importanti del corso quali correttezza, completezza e compattezza). La seconda parte chiede invece lo svolgimento di esercizi (p.e. costruire alberi di derivazione, mostrare modelli o contromodelli per formule, sintetizzare forme normali dalle tabelle di verità). Il superamente della prima parte è pre-requisito alla valutazione della seconda.
Sono previsti i sei appelli canonici (giu-lug, set-ott, gen-feb).
Coloro che non hanno seguito (con successo) le prove di laboratorio e che quindi debbono presentarsi all'orale, così come coloro che vogliono sostenere l'orale per cambiare il voto, debbono concordare con il docente una data per l'orale.
Per presentarsi a un appello è necessario iscriversi nell'apposito sito.Vengono svolte delle esercitazioni usando il software Matita versione 0.5.8 (che non è l'ultima versione).
Testo delle eserctiazioni:
I lucidi sono liberamente scaricabili. Ma evitate di abusare delle stampanti del dipartimento.
Compiti del Dott. Sacerdoti Coen.
Eserciziario del Dott. Dal Lago.
Compiti del Prof. Martini. Quelli il cui nome termina con "sol" sono risolti.