Metodi per il ragionamento automatico
A.A. 2019/2020
Learning objectives
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.
Expected learning outcomes
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.
Course syllabus and organization
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 SilvioProfessor(s)