Publications

Authors:

Bonacina, Maria Paola; Moa, Johansson

Title:

On interpolation in automated theorem proving

Year:

2015

Type of item:

Articolo in Rivista

Tipologia ANVUR:

Articolo su rivista

Language:

Inglese

Format:

A Stampa

Referee:

Sì

Name of journal:

Journal of Automated Reasoning

ISSN of journal:

0168-7433

N° Volume:

54

Number or Folder:

1

:

Kluwer

Page numbers:

69-97

Keyword:

Interpolation Systems; Resolution; Superposition

Short description of contents:

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

Web page:

http://profs.sci.univr.it/~bonacina/interpolation.html; http://profs.sci.univr.it/~bonacina/pub_jou.html; http://profs.sci.univr.it/~bonacina/worksbydate.html; https://link.springer.com/article/10.1007/s10817-014-9314-0; http://doi.org/10.1007/s10817-014-9314-0

Product ID:

83332

Handle IRIS:

11562/801564

Deposited On:

October 22, 2014

Last Modified:

May 18, 2021

Bibliographic citation:

Bonacina, Maria Paola; Moa, Johansson, On interpolation in automated theorem proving «Journal of Automated Reasoning» , vol. 54 , n. 1 , 2015 , pp. 69-97

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