Logica per l'Informatica

Docente: Dott. Claudio Sacerdoti Coen

Informazioni generali:

L'orario di ricevimento e gli avvisi agli studenti sono pubblicati sul sito istituzionale del docente.

Regolamento del corso:

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. Non è possibile utilizzare appunti durante l'esame scritto. La prima parte 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.

Esami:

Sono previsti i sei appelli canonici (3 a giu-lug, 1 a set-ott, 2 a gen-feb). Per le iscrizioni e le date degli appelli fare riferimento a almaesami.

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.

Gli esami non superati verranno comunque registrati come "respinto" sul libretto.

Attività in laboratorio:

Vengono svolte delle esercitazioni usando il software Matita versione 0.5.9 (che non è l'ultima versione ma è scaricabile dalla pagina di Matita).

Chi volesse esercitarsi con Matita da casa può:

  1. Connettersi remotamente alle macchine del laboratorio tramite ssh da una macchina Linux o dopo aver installato un X server. Esistono implementazioni di entrambi i software sia per ambiente Windows che Mac.
  2. Lanciare Matita dentro a una macchina virtuale configurata con l'immagine delle macchine usate in laboratorio.

Testo delle esercitazioni:

Lucidi:

I lucidi sono liberamente scaricabili. Ma evitate di abusare delle stampanti del dipartimento.

I lucidi degli scorsi anni sono disponibili. Tuttavia è possibile che i nuovi lucidi siano anche molto diversi da quelli degli anni precedenti.

Valutazioni (esami e laboratorio):

Valutazioni relative all'attività di laboratorio, voti conseguiti nei vari appelli e voto proposto..

Nota: il voto finale è la somma del voto dello scritto e di quello di laboratorio, quando il primo sia sufficiente. In caso di scritto lievemente insufficiente (maggiore o uguale a 16), è possibile verbalizzare il 18 rinunciando a sommare il punteggio del laboratorio. In caso di scritto maggiore o uguale a 16 e di laboratorio non sostenuto, è necessario presentarsi a un orale integrativo obbligatorio. Una volta raggiunta la sufficienza allo scritto è anche possibile sostenere un orale facoltativo per modificare il punteggio.

Compiti dati agli esami di linguaggi:

Il compito logica2016-2017.pdf mostra la tipologia di esercizi dati agli esami nell'anno accademico 2016-2017, con relativi pesi.

Compiti del Dott. Sacerdoti Coen.

Compiti dati agli esami di logica negli anni precedenti:

Compiti del Prof. Asperti.

Eserciziario del Dott. Dal Lago.

Compiti del Prof. Martini. Quelli il cui nome termina con "sol" sono risolti.