Programma del corso:
la nozione di procedura di prova come combinazione di sistema di
inferenza e piano di ricerca; il teorema di Herbrand;
strategie basate sulla generazione di istanze: dal metodo di Gilmore
alla combinazione di hyperlinking con l'algoritmo di
Davis-Putnam-Logemann-Loveland;
strategie basate sugli ordinamenti ben fondati: schemi di inferenza
di espansione (risoluzione, paramodulazione, sovrapposizione)
e di contrazione (sussunzione, riscrittura) e piani di ricerca
per il ragionamento in avanti;
strategie basate sulla riduzione di goals: risoluzione lineare,
tableaux, eliminazione di modelli e piani di ricerca per il
ragionamento all'indietro;
progetto e uso di dimostratori di teoremi;
cenni di costruzione di modelli;
cenni sulle applicazioni del ragionamento automatico alla
matematica e alla verifica.