Titolo insegnamento in inglese: Logics for computer science
Lingua: italiano
Insegnamento: Logics for computer science
Anno di corso: II
CFU: 6
Semestre: 1
Docenti:
- Canale unico: Guglielmo Tamburrini
Insegnamenti propedeutici previsti
nessuno
Obiettivi Formativi
Acquisire una conoscenza delle principali proprietà sintattiche e semantiche della logica classica proposizionale e della logica del primo ordine. Acquisire familiarità con i principali sistemi deduttivi della logica classica che sono di interesse per l’informatica. Acquisire la capacità di formalizzare enunciati dichiarativi e problemi nel linguaggio della logica classica, nonché di verificare la correttezza di un ragionamento informale.
Contenuti
Logica proposizionale: sintassi e semantica. Forme normali congiuntiva e disgiuntiva. La deduzione naturale. Calcolo dei sequenti. Tableaux analitici. Risoluzione, procedura di Davis-Putnam e metodo refutazionale. Correttezza, completezza e compattezza della logica proposizionale. Logica del primo ordine: elementi di sintassi e di semantica tarskiana. Tableaux analitici. Universo di Herbrand, clausole ground e metodo refutazionale. Formalizzazione e verifica formale di ragionamenti informali. Forma normale prenessa e skolemizzazione. Correttezza, completezza e compattezza della logica del primo ordine. Teorema di Skolem-Lowenheim e modelli non-standard. Cenni ai teoremi di incompletezza di Goedel. Dimostrabilità, verità e insiemi ricorsivamente enumerabili.
Modalità didattiche
Lezioni frontali ad argomento teorico ed esercitazioni per la soluzione di esercizi e problemi elementari di logica.
Modalità di esame
L'esame si articola in prova scritta e orale.
La prova scritta è a risposta libera e con esercizi numerici.