Orario di ricevimento: ogni venerdì alle 15: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.Il software Matita è scaricabile dalla propria home page. Vengono messi a disposizione pacchetti Ubuntu, pacchetti Debian e un live CD per gli utenti di altri sistemi operativi. Attenzione: i pacchetti presenti nelle distribuzioni stable, sia Debian che Ubuntu, sono datati.
I lucidi sono liberamente scaricabili. Ma evitate di abusare delle stampanti del dipartimento.
Valutazioni relative all'attività di laboratorio, voti conseguiti nei vari appelli e voto proposto, in formato ODS.
L'esercitazione consiste nell'utilizzo del dimostratore interattivo di teoremi Matita al fine di dimostrare il principio di dualità per il calcolo proposizionale. La dimostrazione consiste nel:
Il testo dettagliato dell'esercizio con le istruzioni per la consegna è disponibile qui.
È inoltre disponibile una spiegazione dettagliata dell'esercitazione che enuncia le linee guida della prova.
L'esercitazione consiste nell'utilizzo del dimostratore interattivo di teoremi Matita al fine di dimostrare il teorema di espansione di Shannon per il calcolo proposizionale.
Il testo dettagliato dell'esercizio con le istruzioni per la consegna è disponibile qui.
È inoltre disponibile una spiegazione dettagliata dell'esercitazione che enuncia le linee guida della prova.
L'esercitazione consiste nell'utilizzo del dimostratore interattivo di teoremi Matita come correttore di alberi di derivazione per la logica proposizionale.
Il testo dettagliato dell'esercizio con le istruzioni per la consegna è disponibile qui.
È inoltre disponibile una spiegazione dettagliata dell'esercitazione che enuncia le linee guida della prova.
L'esercitazione consiste nell'utilizzo del dimostratore interattivo di teoremi Matita come correttore di alberi di derivazione per la logica proposizionale.
Il testo dettagliato dell'esercizio con le istruzioni per la consegna è disponibile qui.
È inoltre disponibile una spiegazione dettagliata dell'esercitazione che enuncia le linee guida della prova.
L'esercitazione consiste nell'utilizzo del dimostratore interattivo di teoremi Matita come correttore di alberi di derivazione per la logica proposizionale.
Il testo dettagliato dell'esercizio con le istruzioni per la consegna è disponibile qui.
È inoltre disponibile una spiegazione dettagliata dell'esercitazione che enuncia le linee guida della prova.
SOLUZIONE- ->L'esercitazione consiste nell'utilizzo del dimostratore interattivo di teoremi Matita come correttore di alberi di derivazione per la logica del primo ordine.
Il testo dettagliato dell'esercizio con le istruzioni per la consegna è disponibile qui.
È inoltre disponibile una spiegazione dettagliata dei comandi da utilizzare nell'esercitazione.
SOLUZIONE- ->L'esercitazione consiste nell'utilizzo del dimostratore interattivo di teoremi Matita come correttore di alberi di derivazione per la logica del primo ordine. In particolare, si richiede di effettuare una semplice dimostrazione nella teoria dell'aritmetica di Peano.
Il testo dettagliato dell'esercizio con le istruzioni per la consegna è disponibile qui.
È inoltre disponibile una spiegazione dettagliata dei comandi da utilizzare nell'esercitazione.
SOLUZIONE - ->Compiti del Dott. Sacerdoti Coen.
Eserciziario del Dott. Dal Lago.
Compiti del Prof. Martini. Quelli il cui nome termina con "sol" sono risolti.