Metodi per il ragionamento automatico

A.A. 2021/2022
6
Crediti massimi
52
Ore totali
SSD
MAT/01
Lingua
Italiano
Obiettivi formativi
L'insegnamento si propone di introdurre lo studente alle principali tecniche di ragionamento automatico, basate sia su tecniche di saturazione e completamento, che su tecniche di backtracking. Sono previsti sbocchi applicativi sia verso l'algebra computazionale che verso la verifica di sistemi informatici.
Risultati apprendimento attesi
Saper utilizzare, conoscendone i principi di funzionamento, strumenti quali SMT-solvers e superposition provers.
Programma e organizzazione didattica

Edizione unica

Responsabile
Periodo
Secondo semestre
Programma
Risoluzione e teorema di Herbrand; comnpletezza tramite lifting lemma; ordini di riduzione, algoritmo di Knuth Bendix e superposition calculus.
DPLL e DPLL(T) con euristiche; combinazione ed esempi di procedure di decisione.
Basi di Groebner e algoritmo di Buchberger.
Eliminazione dei quantificatiori in domini numerici
Prerequisiti
Non ci sono particolari prerequisiti sulle parti di logica; la parte di algebra computazionale richiede elementari conoscenze sulle principali strutture algebriche.
Metodi didattici
Lezione frontale, attività di laboratorio sui software del corso
Materiale di riferimento
Dispense a cura del docente (disponibili in Ariel).
Software di riferimento: SPASS, z3
Modalità di verifica dell’apprendimento e criteri di valutazione
Durante il corso si terranno attività di laboratorio (senza valutazione, ma obbligatorie); l'esame sarà orale.
MAT/01 - LOGICA MATEMATICA - CFU: 6
Esercitazioni: 12 ore
Laboratori: 12 ore
Lezioni: 28 ore
Docente: Ghilardi Silvio
Docente/i
Ricevimento:
venerdì alle 11,30
Dipartimento di Matematica, via C. Saldini 50