Metodi per il ragionamento automatico
A.A. 2025/2026
Learning objectives
L'insegnamento si propone di fornire allo studente le tecniche di base del calcolo parallelo per il trattamento di problemi provenienti dell'approssimazione di equazioni alle derivate parziali, e dell'algebra lineare numerica in generale.
Expected learning outcomes
Saper utilizzare, conoscendone i principi di funzionamento, strumenti quali SMT-solvers e superposition provers.
Periodo: Secondo semestre
Modalità di valutazione: Esame
Giudizio di valutazione: voto verbalizzato in trentesimi
Corso singolo
Questo insegnamento non può essere seguito come corso singolo. Puoi trovare gli insegnamenti disponibili consultando il catalogo corsi singoli.
Course syllabus and organization
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. Agli studenti non frequentanti verranno assegnati dei progetti.
MAT/01 - LOGICA MATEMATICA - CFU: 6
Esercitazioni: 12 ore
Laboratori: 12 ore
Lezioni: 28 ore
Laboratori: 12 ore
Lezioni: 28 ore
Docente:
Ghilardi Silvio
Professor(s)