Metodi per il ragionamento automatico
A.A. 2024/2025
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.
Periodo: Secondo semestre
Corso singolo
Questo insegnamento non può essere seguito come corso singolo. Puoi trovare gli insegnamenti disponibili consultando il catalogo corsi singoli.
Programma e organizzazione didattica
Edizione unica
Responsabile
Periodo
Secondo semestre
Programma
Risoluzione e teorema di Herbrand; completezza tramite lifting lemma; ordini di riduzione, algoritmo di Knuth Bendix e superposition calculus. Completezza del superposition calculus tramite model generation.
DPLL e DPLL(T) con euristiche; combinazione ed esempi di procedure di decisione.
Sistemi di riscrittura astratti, applicazioni all'algebra computazionale.
Eliminazione dei quantificatori nell'aritmetica lineare reale e intera.
Procedure di decisione mediante automi nella logica monadica del secondo ordine.
Sistemi di riscrittura astratti, applicazioni all'algebra computazionale.
DPLL e DPLL(T) con euristiche; combinazione ed esempi di procedure di decisione.
Sistemi di riscrittura astratti, applicazioni all'algebra computazionale.
Eliminazione dei quantificatori nell'aritmetica lineare reale e intera.
Procedure di decisione mediante automi nella logica monadica del secondo ordine.
Sistemi di riscrittura astratti, applicazioni all'algebra computazionale.
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
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
Laboratori: 12 ore
Lezioni: 28 ore
Docente:
Ghilardi Silvio
Turni:
Turno
Docente:
Ghilardi SilvioDocente/i
Ricevimento:
venerdì alle 11,30
Dipartimento di Matematica, via C. Saldini 50