Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
From MaRDI portal
Publication:5892495
DOI10.1007/978-3-642-19835-9_13zbMath1315.68179arXiv1010.4422OpenAlexW2114754094MaRDI QIDQ5892495
Roberto Sebastiani, Alberto Griggio, Thi Thieu Hoa le
Publication date: 19 May 2011
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/1010.4422
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (5)
Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic ⋮ Interpolation and Model Checking ⋮ An interpolating sequent calculus for quantifier-free Presburger arithmetic ⋮ Complete instantiation-based interpolation ⋮ Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
Uses Software
Cites Work
- Unnamed Item
- Constraint solving for interpolation
- An interpolating theorem prover
- Efficient generation of craig interpolants in satisfiability modulo theories
- Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations
- Interpolants for Linear Arithmetic in SMT
- Ground Interpolation for the Theory of Equality
- 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
- Interpolating Quantifier-Free Presburger Arithmetic
- Ground Interpolation for Combined Theories
- Splitting on Demand in SAT Modulo Theories
- Automated Deduction – CADE-20
- An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic
This page was built for publication: Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
