Pubblicazioni

On interpolation in automated theorem proving  (2015)

Autori:
Bonacina, Maria Paola; Moa, Johansson
Titolo:
On interpolation in automated theorem proving
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:
1
Editore:
Kluwer
Intervallo pagine:
69-97
Parole chiave:
Interpolation Systems; Resolution; Superposition
Breve descrizione dei contenuti:
Given two inconsistent formulae, a (reverse) interpolant is a formula implied by one, inconsistent with the other, and only containing symbols they share. Interpolation finds application in program analysis, verification, and synthesis, for example, towards invariant generation. An interpolation system takes a refutation of the inconsistent formulae and extracts an interpolant by building it inductively from partial interpolants. Known interpolation systems for ground proofs use colors to track symbols. We show by examples that the color-based approach cannot handle non-ground refutations by resolution and paramodulation/superposition. We present a two-stage approach that works by tracking literals, computes a provisional interpolant, which may contain non-shared symbols, and applies lifting to replace non-shared constants by quantified variables. We obtain an interpolation system for non-ground refutations, and we prove that it is complete, if the only non-shared symbols in provisional interpolants are constants.
Note:
Published online on 19 October 2014
Pagina Web:
https://link.springer.com/article/10.1007/s10817-014-9314-0
http://doi.org/10.1007/s10817-014-9314-0
https://mariapaola.github.io/
Id prodotto:
83332
Handle IRIS:
11562/801564
depositato il:
22 ottobre 2014
ultima modifica:
15 settembre 2023
Citazione bibliografica:
Bonacina, Maria Paola; Moa, Johansson, On interpolation in automated theorem proving «Journal of Automated Reasoning» , vol. 54 , n. 12015pp. 69-97

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