Pubblicazioni

Interpolation systems for ground proofs in automated deduction: a survey  (2015)

Autori:
Bonacina, Maria Paola; Moa, Johansson
Titolo:
Interpolation systems for ground proofs in automated deduction: a survey
Anno:
2015
Tipologia prodotto:
Articolo in Rivista
Tipologia ANVUR:
Articolo su rivista
Lingua:
Inglese
Formato:
A Stampa
Referee:
Nome rivista:
Journal of Automated Reasoning
ISSN Rivista:
0168-7433
N° Volume:
54
Numero o Fascicolo:
4
Editore:
Kluwer
Intervallo pagine:
353-390
Parole chiave:
Automated theorem proving; Satisfiability modulo theories; Superposition-based inference systems
Breve descrizione dei contenuti:
Interpolation is a deductive technique applied in program analysis and verification: for example, it is used to compute over-approximations of images orrefine abstractions. An interpolation system takes a refutation and extracts an interpolant by building it inductively from partial interpolants. We survey color-based interpolation systems for ground proofs produced by key inference engines of state-of-the-art solvers: DPLL for propositional logic, equality sharing for combination of convex theories, and DPLL(T) for SMT-solving. Since color-based interpolation systems use colors to track symbols in proofs, equality is problematic, because replacement of equals by equals mixes symbols and therefore colors. We analyze interpolation in the presence of equality, and we demonstrate the color-based approach by giving a complete interpolation system for ground proofs by superposition.
Note:
Published online 20 March 2015
Pagina Web:
http://dx.doi.org/10.1007/s10817-015-9325-5
https://link.springer.com/article/10.1007/s10817-015-9325-5
https://mariapaola.github.io/
Id prodotto:
86268
Handle IRIS:
11562/900586
depositato il:
3 marzo 2015
ultima modifica:
15 settembre 2023
Citazione bibliografica:
Bonacina, Maria Paola; Moa, Johansson, Interpolation systems for ground proofs in automated deduction: a survey «Journal of Automated Reasoning» , vol. 54 , n. 42015pp. 353-390

Consulta la scheda completa presente nel repository istituzionale della Ricerca di Ateneo IRIS

Progetti Collegati
Titolo Dipartimento Responsabili
Integrazione di metodi di ragionamento automatico nel model checking: verifica formale automatica di sistemi di grande scala e a stati infiniti - Progetto ed integrazione di macchine di prova per l'analisi di programmi (PRIN 2007) Dipartimento Informatica Maria Paola Bonacina
<<indietro

Attività

Strutture

Condividi