Logics for computer science

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.

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.