Corso di Logica matematica - a.a.1995/96
(Corso di Laurea in Informatica)
Programma del Corso
Linguaggi e interpretazioni
Linguaggi del prim'ordine ad una o piu' sorte di individui. Nozioni
sintattiche: termini, formule,
enunciati, sostituzioni, chiusure universali e esistenziali.
Interpretazioni: verità in un'interpretazione, lemma di
sostituzione, equivalenza semantica,
rinomine e sostituibilità di sottoformule equivalenti.
Forme prenesse, normali congiuntive e disgiuntive, forme clausali.
Algoritmi di trasformazione;
correttezza, completezza, e terminazione forte.
Soddisfacibilità e validità. Conseguenza logica.
Equisoddisfacibilità e Skolemizzazione.
Aggiunta di simboli funzionali- conservatività.
Interpretazioni di Herbrand. Soddisfacibilità di formule universali.
Logica di Horn: asserzioni,
regole e programmi definiti, proprietà dell'intersezione e modello
minimo. Comportamento
costruttivo della relazione di conseguenza logica fra programmi
definiti e chiusure esistenziali
di congiunzioni di atomi.
Relazioni fra interpretazioni: omomorfismo, isomorfismo e elementare
equivalenza. Strutture
quoziente. Logica con uguaglianza, interpretazioni normali,
riducibilità alla logica pura.
Estensioni definitorie.
Il problema della decisione
Caso proposizionale: valutazioni, tautologie e conseguenza tautologica.
Sufficienza di insiemi di connettivi. Tavole di riduzione per giudizi.
Terminazione forte,
correttezza e completezza del metodo. Teorema di compattezza.
Caso predicativo; la procedura di semidecisione per la validità,
teorema di compattezza e di Lowenheim-Skolem.
Sistemi deduttivi
Il sistema di deduzione naturale NI per la logica intuizionistica.
Sviluppi. Equivalenza su NI di
schemi adeguati per la logica classica. Il sistema NC. Correttezza di
NC e sua completezza (solo
enunciato). Eliminabilità della negazione; della costante per il falso.
Introducibilità della
biimplicazione. Sistemi per la logica con uguaglianza.
Risoluzione
La regola di risoluzione. Unificazione. Algoritmo risolutivo di sistemi
di equazioni di Herbrand.
Correttezza e completezza (solo enunciato) della regola di risoluzione
per l'insoddisfacibilità
di insiemi di clausole. Teorema di Herbrand.
