CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

On Interpolation in Automated Theorem Proving

M. P. Bonacina ; Moa Johansson (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers))
Journal of automated reasoning (0168-7433). Vol. 54 (2015), 1, p. 69-97.
[Artikel, refereegranskad vetenskaplig]

Given two inconsistent formul', 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 formul' 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.

Nyckelord: Interpolation systems, Superposition, Resolution



Denna post skapades 2015-01-16. Senast ändrad 2015-12-17.
CPL Pubid: 210919

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)