66857 - LOGICA PER L'INFORMATICA

Scheda insegnamento

Anno Accademico 2017/2018

Conoscenze e abilità da conseguire

Al termine del corso, lo studente conosce il linguaggio del calcolo proposizionale e della logica del prim'ordine. È in grado di scrivere e comprendere proposizioni logiche e di verificarne la validità.

Programma/Contenuti

1. Linguaggi proposizionali: sintassi e semantica. Soddisfacibilità; equivalenze semantiche. Metodi sintattici: Risoluzione proposizionale e Deduzione Naturale. Correttezza e completezza. 2. Linguaggi del prim'ordine. Predicati, termini, quantificatori. Sintassi. Variabili libere e vincolate. Interpretazioni. Semantica per un linguaggio predicativo. Soddisfacibilità e equivalenze semantiche. 3. Induzione matematica. 4. Metodi sintattici del prim'ordine: Deduzione naturale. Teorema di correttezza. Teorema di completezza. Teorema di compattezza.

Gli orari di lezione verranno pubblicati al seguente indirizzo (cercare "LI", Logica per l'Informatica, anche se il corso che seguite ha altri nomi tipo Linguaggi):
http://orari.web.cs.unibo.it/cgi-bin/2013-2014/II-ciclo/inf/primo.php

Testi/Bibliografia

A. Asperti - A. Ciabattoni, Logica a informatica, McGraw Hill, 1997.

Metodi didattici

Il corso si svolge al secondo semestre ed è articolato in lezioni frontali in aula ed esercitazioni settimanali in laboratorio. Durante le lezioni frontali vengono trattati esaustivamente tutti gli argomenti del corso, fornendo dimostrazioni dettagliate della quasi totalità dei teoremi. Durante le esercitazioni di laboratorio viene chiesto allo studente di applicare quanto appreso a lezione alla dimostrazione di nuovi teoremi.

Modalità di verifica dell'apprendimento

La verifica dell'apprendimento si baserà sull'analisi degli elaborati prodotti dagli studenti durante le esercitazioni in laboratorio e su un esame scritto. Lo studente che raggiunga la sufficienza nell'esame scritto potrà effettuare un orale integrativo opzionale sugli stessi argomenti per migliorare la valutazione. L'orale diventa obbligatorio per quegli studenti impossibilitati a frequentare l'attività di laboratorio.

L'attività di laboratorio è mirata all'apprendimento di strumenti di auto-verifica della capacità di produrre dimostrazioni matematiche rigorose. Viene utilizzato il software Matita.

L'esame scritto, della durata di tre ore, si articola in domande di teoria (definizioni, enunciati, dimostrazioni viste a lezione) e esercizi di ragionamento (produzione di nuove dimostrazioni e risoluzione di problemi).

Strumenti a supporto della didattica

I lucidi delle lezioni vengono resi disponibili tramite Web. Inoltre viene fornito il software Matita utilizzato nelle esercitazioni in laboratorio.

Link ad altre eventuali informazioni

http://www.cs.unibo.it/~sacerdot/logica

Orario di ricevimento

Consulta il sito web di Claudio Sacerdoti Coen