Proof tree preserving tree interpolation

DOI10.1007/S10817-016-9365-5MaRDI QIDQ286737zbMATH OpenOpenAlexFDO

Authors Jürgen Christ, Jochen Hoenicke

Publication date 25 May 2016

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-016-9365-5

zbMATH Keywords

SMTproof tree preservationtree interpolation

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Interpolation, preservation, definability (03C40)

Recommendations

• Proof tree preserving interpolation
• Tree Interpolation in Vampire
• Constraint solving for interpolation
• Constraint Solving for Interpolation
• Tools and Algorithms for the Construction and Analysis of Systems

Cites work

• Abstractions from proofs
• An interpolating sequent calculus for quantifier-free Presburger arithmetic
• An interpolating theorem prover
• Automated Deduction – CADE-20
• Complete instantiation-based interpolation
• Computer Aided Verification
• Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers
• Efficient Interpolant Generation in Satisfiability Modulo Theories
• From strong amalgamability to modularity of quantifier-free interpolation
• Inductive data flow graphs
• Interpolant strength
• Interpolation and SAT-based model checking.
• Lazy Abstraction with Interpolants
• Lower bounds for resolution and cutting plane proofs and monotone computations
• Nested interpolants
• On recursion-free Horn clauses and Craig interpolation
• Proof tree preserving interpolation
• Resolution proof transformation for compression and interpolation
• Simplification by Cooperating Decision Procedures
• Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
• Tree Interpolation in Vampire

Cited in

(5)

• Farkas-based tree interpolation
• SMT-based verification of program changes through summary repair
• Proof tree preserving interpolation
• Choose Your Colour: Tree Interpolation for Quantified Formulas in SMT
• Tree Interpolation in Vampire

Describes a project that uses

Uses Software

• FOCI
• SLAB
• SMTInterpol
• Princess
• z3

This page was built for publication: Proof tree preserving tree interpolation

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