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

Interpolation Systems for Ground Proofs in Automated Deduction: a Survey

M.P. Bonacina ; Moa Johansson (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers))
Journal of Automated Reasoning (0168-7433). Vol. 54 (2015), 4, p. 353-390.
[Artikel, refereegranskad vetenskaplig]

Interpolation is a deductive technique applied in program analysis and verification: for example, it is used to compute over-approximations of images or refine 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((Formula presented.)) 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.

Nyckelord: Decision procedures , Interpolation systems , Satisfiability modulo theories , Theory combination



Denna post skapades 2015-06-16. Senast ändrad 2015-12-17.
CPL Pubid: 218444

 

Läs direkt!


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


Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)

Ämnesområden

Inbäddad systemteknik

Chalmers infrastruktur