Corso di Deduzione Automatica

Laurea Specialistica in Logica computazionale

Anno accademico: 2004-2005

Docenti: Stefano Berardi, Gabriele Lolli, Viviana Patti

Numero di ore: 54
Numero di CFU (Crediti Formativi Universitari): 6
Terzo periodo: Aprile-Giugno

INDICE

1. Obiettivi del corso
2. Competenze attese e propedeuticità
3. Come si svolgono le lezioni (supporti alla didattica in uso alla docenza)
4. Programma/contenuti
5. Materiale didattico di supporto
6. Bibliografia (libri, articoli, documenti on-line,...)
7. Controllo dell'appprendimento (durante il corso)
8. Verifica (modalità d'esame)
9. Appelli

1. Obiettivi del corso

Il corso ha l'obiettivo di fornire nozioni di base sui metodi di deduzione automatica, con particolare attenzione alla unificazione e risoluzione, alla base del PROLOG e di ISABELLE.

2. Competenze attese e propedeuticità

• Competenze attese in ingresso (richieste all'inizio del corso). Calcolo dei predicati del primo ordine.
• Eventuali corsi propedeutici (forniscono le "competenze attese in ingresso"). Logica Matematica (laurea triennale), Logiche per Informatica (laurea specialistica).
• Competenze attese in uscita (acquisite durante il corso). Capacità di usare il PROLOG per lo sviluppo di prototipi per la deduzione automatica (in particolare semantic tableax), nonché comprensione e capacità di impiego di sistemi esistenti.

3. Come si svolgono le lezioni

Le lezioni si svolgeranno in aula e in laboratorio.

4. Programma/contenuti

1. la risoluzione e le basi teoriche del PROLOG;
2. tecniche di programmazione PROLOG; implementazione in Sicstus Prolog di metodi di prova tableau-based secondo il metodo LeanTAP
3. risoluzione higher order e ISABELLE.

5. Materiale didattico di supporto

Il materiale didattico di supporto (lucidi, link, ed altro) sono disponibili presso il supporto on-line ai corsi I-learn.

6. Bibliografia

• Per la parte riguradante il calcolo della risoluzione: http://www2.dm.unito.it/paginepersonali/lolli/dispense00.htm
• Luca Console et al., Programmazione logica e PROLOG UTET 1997.
• A.A.V.V. Lean, Tableau-based Deduction
• Reinhold Letz, First-order tableau methods, in M. D'Agostino, D. Gabbay, R. Hähnle and J. Posegga, eds, 'Handbook of Tableau Methods', Kluwer, Dordrecht, pp. 125-196.
• Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel Isabelle/HOL. A Proof Assistant for Higher-Order Logic (vedi in particolare link Isabelle)

7. Controllo dell'apprendimento

Il controllo dell'apprendimento è basato sulle domande che gli studenti fanno durante le ore di lezione e durante i ricevimenti.

8. Verifica (modalità d'esame)

L'esame consiste in una prova orale.

Appelli