Intelligenza Artificiale: Deduzione automatica

Nell'ambito dell'intelligenza artificiale i metodi formali e la deduzione meccanizzata costituiscono una tradizione importante ed un terreno fertile di applicazioni. Il proof-checker Verona è un sistema, che stiamo costruendo in collaborazione con lo Stanford Artificial Intelligence Laboratory, per l'implementazione di processi inferenziali attraverso la trasformazione di una sintassi astratta (Abstract Binding Structures) rappresentata in forme sia testuali che grafiche (lambda calcolo visuale, 1998-99). Il corso consiste di una parte teorica, su temi di logica, teoria della dimostrazione e di teoria della computazione rilevanti al progetto in corso, e di un progetto implementativo, volto a sviluppare nuove proprietà del nostro proof-checker. Il corso è rivolto a studenti degli ultimi anni; esso può preparare ad una tesi di laurea in deduzione meccanizzata oppure fornire tecniche utili ai fini di altre specializzazioni (in intelligenza artificiale, metodi formali, teoria, robotica ecc.)

Programma del corso:

• Fondamenti logici. (Richiami e approfondimenti) Formalizzazione del linguaggio naturale nel calcolo dei predicati. Richiami di sintassi e semantica del calcolo dei predicati. Il calcolo dei sequenti di Gentzen e il metodo dei semantic tableaux. Teorema di completezza di Goedel (richiami). La deduzione naturale di Gentzen. Relazioni fra calcolo dei sequenti e deduzione naturale.
• Lambda Calcolo. Nozioni elementari del lambda calcolo puro e tipato: Sostituzione e beta-conversione, rappresentazione delle funzioni ricorsive, il sistema di tipi intersezione, normalizzazione (Krivine, op.cit. capitoli 1-4.)
• Algoritmi. Algoritmi di unificazione.
• Implementazione. Progetti per lo sviluppo del theorem prover Verona. Programmi Java di deduzione meccanizzata, da definire all'inizio del corso.
• Seminari. Approfondimenti di temi teorici o implementativi da parte di studenti, docenti, visitatori.

Testi di riferimento: J.L. Krivine. Lambda-calcul, types et modèles, Masson, Paris 1990. Trad. inglese Lambda-calculus, types and models, Ellis Horwood, 1993.