Proof tree preserving tree interpolation
From MaRDI portal
Publication:286737
DOI10.1007/S10817-016-9365-5zbMATH Open1356.68184OpenAlexW2293154396MaRDI QIDQ286737FDOQ286737
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
Recommendations
Mechanization of proofs and logical operations (03B35) Interpolation, preservation, definability (03C40)
Cites Work
- Interpolant strength
- Simplification by Cooperating Decision Procedures
- Resolution proof transformation for compression and interpolation
- Nested interpolants
- Interpolation and SAT-based model checking.
- 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
- Lower bounds for resolution and cutting plane proofs and monotone computations
- 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
- On recursion-free Horn clauses and Craig interpolation
Cited In (5)
Uses Software
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)
