Choose Your Colour: Tree Interpolation for Quantified Formulas in SMT
From MaRDI portal
Publication:6492748
DOI10.1007/978-3-031-38499-8_15MaRDI QIDQ6492748
Jochen Hoenicke, Unnamed Author, Tanja I. Schindler
Publication date: 26 April 2024
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- Proof tree preserving tree interpolation
- Cuts from proofs: a complete and practical technique for solving linear inequalities over integers
- On recursion-free Horn clauses and Craig interpolation
- Cell morphing: from array programs to array-free Horn clauses
- On interpolation in automated theorem proving
- Splitting proofs for interpolation
- Tree Interpolation in Vampire
- Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
- Abstraction Refinement for Quantified Array Assertions
- Abstractions from proofs
- Lower bounds for resolution and cutting plane proofs and monotone computations
- First-Order Interpolation and Interpolating Proof Systems
- Interpolation Properties and SAT-Based Model Checking
- Nested interpolants
- Tools and Algorithms for the Construction and Analysis of Systems
- Thread modularity at many levels: a pearl in compositional verification
- An Efficient and Flexible Approach to Resolution Proof Reduction
- Automated Deduction – CADE-20
- Predicate abstraction and refinement for verifying multi-threaded programs
- Quantified Invariant Generation Using an Interpolating Saturation Prover
- Verification, Model Checking, and Abstract Interpretation
This page was built for publication: Choose Your Colour: Tree Interpolation for Quantified Formulas in SMT
