Proof tree preserving tree interpolation

DOI10.1007/s10817-016-9365-5zbMath1356.68184OpenAlexW2293154396MaRDI QIDQ286737

Jochen Hoenicke, Jürgen Christ

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)

Related Items

SMT-based verification of program changes through summary repair, Farkas-based tree interpolation

Uses Software

• z3
• Princess
• SMTInterpol
• SLAB
• FOCI

Cites Work

• Resolution proof transformation for compression and interpolation
• On recursion-free Horn clauses and Craig interpolation
• An interpolating theorem prover
• Tree Interpolation in Vampire
• From Strong Amalgamability to Modularity of Quantifier-Free Interpolation
• Inductive data flow graphs
• Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
• Abstractions from proofs
• Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers
• Interpolant Strength
• Simplification by Cooperating Decision Procedures
• Lower bounds for resolution and cutting plane proofs and monotone computations
• Nested interpolants
• Computer Aided Verification
• Proof Tree Preserving Interpolation
• Automated Deduction – CADE-20
• Efficient Interpolant Generation in Satisfiability Modulo Theories
• An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic
• Lazy Abstraction with Interpolants
• Complete instantiation-based interpolation
• Computer Aided Verification