L'esistenza stessa dell'informatica dipende dalla capacità di rappresentare adeguatamente nozioni ed elaborarle attraverso opportune trasformazioni delle loro rappresentazioni. Detto altrimenti l'elaborazione delle conoscenze si appoggia sulle distinzioni 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.
- Richiami a strutture, linguaggi formali del primo ordine, definizione base 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 agli alberi 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.
- Isomorfismo, immersione, immersione elementare, elementare equivalenza.
- Cenni alla deduzione naturale.
- Forme normali.
- Deduzione alla Hilbert. Teorema di deduzione. Insiemi massimali consistenti. Insiemi di Henkin.
- Teoremi di validità e completezza per la deduzione alla Hilbert.
Possibilità di sostenere prove parziali utili alla valutazione finale.
Prova finale con risposta a domande varie (teoriche, applicative, ecc.) in modalità scritta. Eventuale integrazione orale per ottenere voti superiori ai 27/30.
******** CSS e script comuni siti DOL - frase 9957 ********p>