Metodi per il ragionamento automatico
A.A. 2019/2020
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
- Skolemizzazione e riduzione a forma clausale. L'algoritmo di unificazione
e il calcolo della risoluzione. Teorema di completezza refutazionale.
- Ordinamenti e vincoli di ordinamento. La risoluzione ordinata.
- Paramodulazione e Sovrapposizione. Regole di riduzione. Struttura di un
dimostratore automatico.
- Problemi della parola: coppie critiche, completamento, algoritmo di
Knuth-Bendix. Presentazioni finite di gruppi e monoidi. Basi di Groebner e
algoritmo di Buchberger.
- Problemi SAT; la procedura DPLL. Backtracking non cronologico, CDCL e
altre euristiche.
- Da SAT a SMT; esempi di procedure di decisione. Combinazione di
procedure di decisione. Lo standard SMT-LIB.
- Applicazioni al model-checking per sistemi a stati infiniti. Esempi di
verifica automatica di proprietà di programmi sequenziali e di protocolli
distribuiti
e il calcolo della risoluzione. Teorema di completezza refutazionale.
- Ordinamenti e vincoli di ordinamento. La risoluzione ordinata.
- Paramodulazione e Sovrapposizione. Regole di riduzione. Struttura di un
dimostratore automatico.
- Problemi della parola: coppie critiche, completamento, algoritmo di
Knuth-Bendix. Presentazioni finite di gruppi e monoidi. Basi di Groebner e
algoritmo di Buchberger.
- Problemi SAT; la procedura DPLL. Backtracking non cronologico, CDCL e
altre euristiche.
- Da SAT a SMT; esempi di procedure di decisione. Combinazione di
procedure di decisione. Lo standard SMT-LIB.
- Applicazioni al model-checking per sistemi a stati infiniti. Esempi di
verifica automatica di proprietà di programmi sequenziali e di protocolli
distribuiti
Prerequisiti
Non sono richieste conoscenze preliminari.
Metodi didattici
Lezioni frontali ed esercitazioni in aula informatizzata
Materiale di riferimento
Verranno fornite sulla piattaforma Ariel dispense e/o appunti a cura del docente a copertura dei contenuti del corso. Si utilizzeranno strumenti software (superposition provers, SMT-solvers, model-checkers) disponibili gratuitamente in rete per usi non commerciali; per i relativi link si consulti la piattaforma Ariel.
Modalità di verifica dell’apprendimento e criteri di valutazione
L'esame consiste di una prova orale, durante la quale verrà richiesto di illustrare alcuni risultati e applicazioni inerenti al programma dell'insegnamento, al fine di valutare le conoscenze e la comprensione degli argomenti trattati, nonché la capacità di saperli utilizzare. Alla valutazione concorrerà anche la partecipazione a esercitazioni collettive in aula informatizzata. Il voto è espresso in trentesimi e verrà comunicato immediatamente al termine della prova orale.
MAT/01 - LOGICA MATEMATICA - CFU: 6
Esercitazioni: 10 ore
Laboratori: 12 ore
Lezioni: 28 ore
Laboratori: 12 ore
Lezioni: 28 ore
Docente:
Ghilardi Silvio
Turni:
-
Docente:
Ghilardi SilvioDocente/i