Docente
- Giovanna D'Agostino
PROGRAMMA
Il metodo di risoluzione per logica classica proposizionale:
correttezza e completezza nel caso finito.
Teorema di compattezza e completezza di risoluzione;
Clausole di Horn e LD refutazioni;
Programmi Prolog e SLD ref. (indipendenza dalla regola di selezione).
Logica predicativa, notazione con simboli funzionali;
Forma Prenessa e Skolemizzazione;
Modelli di Herbrand.
Teorema di Herbrand;
Teorema di Compattezza, esempi;
Algoritmo di Unificazione: terminazione.
Algoritmo di unificazione: correttezza e completezza;
Risoluzione Predicativa: corrrettezza e completezza (lifting Lemma).
SLD refutazione: cenni alla completezza;
indecidibilita' del calcolo dei predicati: programmi prolog e macchine a registri.
Problemi di Espressivita'. Proprieta' che non sono esprimibili al prim'ordine:
giochi di Ehrenfeucht-Fraisse'.
- Logic for Application; A.Nerode,R,Shore, Springer Verlag (i capitoli relatvi al programma)
dispense sui giochi
(primi due capitoli)