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.
Prerequisiti
No
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
Frequenza delle lezioni ed esercitazioni: Raccomandata
Strumenti a supporto della didattica
UniFi E-Learning: http://e-l.unifi.it
Orario di ricevimento:
Su appuntamento.
Tel. 055 4598751 - 4598752
Fax. 055 4598930
E_mail: gianni.aguzzi@unifi.it
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.