Metodi per il ragionamento automatico
A.A. 2018/2019
Obiettivi formativi
Obiettivi
Il corso si propone di sviluppare le principali tecniche di ragionamento
automatico, basate sia su metodi di saturazione e completamento, che su
metodi di backtracking. Lo studente verrà introdotto all'utilizzo di alcuni
strumenti informatici quali superposition provers, SAT- e SMT-solvers,
model finders, model-checkers. Sono previsti sbocchi applicativi sia verso
l'algebra computazionale che verso la verifica di sistemi informatici.
Il corso si propone di sviluppare le principali tecniche di ragionamento
automatico, basate sia su metodi di saturazione e completamento, che su
metodi di backtracking. Lo studente verrà introdotto all'utilizzo di alcuni
strumenti informatici quali superposition provers, SAT- e SMT-solvers,
model finders, model-checkers. Sono previsti sbocchi applicativi sia verso
l'algebra computazionale che verso la verifica di sistemi informatici.
Risultati apprendimento attesi
Al termine del corso lo studente avrà acquisito familiarità con alcuni
sistemi per il ragionamento automatico, quali superposition provers
(SPASS, Eprover), SMT solvers (Z3, Yices, MathSat) e model-checkers per
sistemi a stati infiniti (muZ, nuXmv, MCMT).
sistemi per il ragionamento automatico, quali superposition provers
(SPASS, Eprover), SMT solvers (Z3, Yices, MathSat) e model-checkers per
sistemi a stati infiniti (muZ, nuXmv, MCMT).
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.
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
Propedeuticità
Logica Matematica I (non indispensabile), Algebra I
Prerequisiti
Esame Orale
Metodi didattici
Modalità di frequenza:
Consigliata
Consigliata
Materiale di riferimento
Verranno fornite 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.
contenuti del corso. Si utilizzeranno strumenti software (superposition
provers, SMT-solvers, model-checkers) disponibili gratuitamente in rete per
usi non commerciali.
INF/01 - INFORMATICA - CFU: 6
Esercitazioni: 10 ore
Laboratori: 12 ore
Lezioni: 28 ore
Laboratori: 12 ore
Lezioni: 28 ore
Docente:
Ghilardi Silvio
Docente/i