Teoria della dimostrazione: metodi del ragionamento automatico

Scuola Italiana di Logica 2005

Docente: Maria Paola Bonacina (mariapaola.bonacina@univr.it)

Obbiettivi formativi:
Il corso assume conoscenze di logica ed algoritmi quali quelle impartite dai corsi di laurea di I livello, e presenta problemi, metodi e sistemi di ragionamento automatico, combinando fondamenti teorici con questioni pratiche di natura algoritmico-implementativa, in modo da preparare lo studente a progettare, valutare ed applicare metodi e sistemi di ragionamento automatico.

Programma del corso:
procedura di prova come combinazione di sistema di inferenza e piano di ricerca, derivazione, limite di una derivazione; il teorema di Herbrand; l'algoritmo di Davis-Putnam-Logemann-Loveland (DPLL) per la soddisfacibilità proposizionale; l'universo di Herbrand come insieme ordinato: ordinamenti di riduzione e di semplificazione, loro proprietà, ordinamenti ricorsivi a cammini; strategie basate sugli ordinamenti ben fondati: regole di inferenza di espansione (risoluzione, paramodulazione, sovrapposizione) e di contrazione (sussunzione, semplificazione clausale, semplificazione equazionale o riscrittura); strategie basate sulla generazione di istanze: dal metodo di Gilmore alla combinazione di hyperlinking con DPLL; esempi d'uso di dimostratori di teoremi.

Bibliografia:



Maria Paola Bonacina