Obiettivi formativi
L'esistenza stessa dell'informatica dipende dalla capacità
di rappresentare adeguatamente nozioni ed elaborarle attraverso
opportune trasformazionidelle loro rappresentazioni. Detto
altrimenti l'informatica dipende dalledistinzioni e legami tra
semantica e sintassi. Lo scopo di questo insegnamentoè
l'evidenziazione e lo studio del rapporto tra semantica e
sintassi,mettendo in luce potenzialità e limiti dei
linguaggi formali.
Attività formative
Il corso viene svolto in 54 ore di lezione/esercitazione frontale.
Programma del corso
Richiami a strutture, linguaggi formali del primo ordine,
definizionebase di verità in una realizzazione,
soddisfacibilità, validità, conseguenza logica. Il
problema del controllo sintattico della soddisfacibilità.
Alberi di confutazione per l'analisi delle formule a blocchi.
Insiemi di Hintikka.Teoremi di validità, di completezza e di
compattezza rispetto aglialberi di confutazione. Teoremi di
Lowenheim Skolem. Categoricità e alfa
categoricità. Paradosso di Skolem. Linguaggi numerabili e
alberi per l'analisi delle formule una ad una. Cenni alla deduzione
naturale. Forme normali. Il metodo di risoluzione. Deduzione alla
Hilbert. Teorema di deduzione. Insiemi massimali consistenti.
Insiemi di Henkin. Teoremi di validità e completezza per la
deduzione alla Hilbert.