Unificazione fra termini. Calcolo di Hilbert, forme clausali,Algebra di Herbrand, Teoremi di Herbrand.Calcolo della Risoluzione, sua Correttezza e Completezza. Clausole di Horn, la Programmazione Logica e la Risoluzione SLD. Semantica Operazionale e a Modelli della Programmazione Logica. Il problema della negazione: La Risoluzione SLDNF. Il linguaggio Prolog. Applicazioni: manipolazione di termini; liste-differenza, le DCG; costruzione di metainterpreti per il Prolog.
L. Console, E. Lamma, P. Mello, M. Milano - Programmazione Logica e Prolog, Utet, Torino
V. Sperschneider, G. Antoniou - Logic: A Foundation for Computer Science, Addison Wesley Pub. Co.
J.W. LLoyd - Foundations of Logic Programming, Springer Verlag
K.R. Apt - From Logic Programming to Prolog, Prentice Hall,1997
Obiettivi Formativi
Conoscenze:
Basi teoriche (unificazione di termini, principio di risoluzione) e pratiche applicazioni del paradigma di programmazione dichiarativo basato sulla logica dei predicati. Linguaggio di programmazione Prolog.
Competenze acquisite
Uso appropriato del paradigma di programmazione dichiarativo, in particolare uso del concetto di ricorsione e rappresentazione dell’informazione tramite termini nella soluzione di vari problemi.
Capacità acquisite al termine del corso:
Realizzazione di un progetto quale soluzione di un problema concreto utilizzando le metodologie della programmazione logica e la conoscenza del linguaggio Prolog.
Metodi Didattici
Numero di ore totali del corso: 150
Numero di ore per studio personale e altre attività formative di tipo individuale: 102
Numero di ore relative alle attività in aula: 48
Altre Informazioni
Martedi’ dalle ore 14.00 alle ore 16.00 nel suo studio.
Orario di ricevimento
Modalità di verifica apprendimento
Modalità:
Prova orale e discussione di un elaborato (in Prolog).
Programma del corso
Contenuti del corso (programma dettagliato):
Unificazione sintattica fra termini e sua decidibilita'.
Teoria della dimostrazione. Calcolo di Hilbert. Forme Normali di formule, forma clausale.
Algebra di Herbrand e Teoremi di Herbrand. Dimostrazione per refutazione, Calcolo della Risoluzione per Clausole Generali, sua Correttezza e Completezza.
Logica a clausole di Horn.
La Programmazione Logica e la Risoluzione SLD.
Semantica Operazionale e a Modelli della Programmazione Logica. La negazione: Risoluzione SLDNF.
Il linguaggio Prolog.
Applicazioni: liste-differenza e le DCG, manipolazione di termini,costruzione di interpreti e/o compilatori.