Proof tree preserving interpolation

DOI10.1007/978-3-642-36742-7_9MaRDI QIDQ5326320zbMATH OpenOpenAlexFDO

Authors Jürgen Christ, Jochen Hoenicke, Alexander Nutz

Publication date 5 August 2013

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1705.05309

Mathematics Subject Classification ID

Logic in computer science (03B70) Interpolation, preservation, definability (03C40) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: Craig interpolation in SMT is difficult because, e. g., theory combination and integer cuts introduce mixed literals, i. e., literals containing local symbols from both input formulae. In this paper, we present a scheme to compute Craig interpolants in the presence of mixed literals. Contrary to existing approaches, this scheme neither limits the inferences done by the SMT solver, nor does it transform the proof tree before extracting interpolants. Our scheme works for the combination of uninterpreted functions and linear arithmetic but is extendable to other theories. The scheme is implemented in the interpolating SMT solver SMTInterpol.

Recommendations

• Proof tree preserving tree interpolation
• Efficient generation of Craig interpolants in satisfiability modulo theories
• Ground Interpolation for Combined Theories
• Efficient Interpolant Generation in Satisfiability Modulo Theories
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(11)

• Farkas-based tree interpolation
• Automated program verification
• Petri Net Synthesis for Restricted Classes of Nets
• A survey of satisfiability modulo theory
• Proof tree preserving tree interpolation
• Weakly equivalent arrays
• Satisfiability modulo theories
• Resolution proof transformation for compression and interpolation
• Target-oriented Petri net synthesis
• Complete instantiation-based interpolation
• Interpolation Results for Arrays with Length and MaxDiff

This page was built for publication: Proof tree preserving interpolation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5326320)