Interpolants for Linear Arithmetic in SMT

DOI10.1007/978-3-540-88387-6_13zbMath1183.68379OpenAlexW1500752789MaRDI QIDQ3540071

No author found.

Publication date: 20 November 2008

Published in: Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-88387-6_13

Mathematics Subject Classification ID

Related Items (5)

Preface: Special issue on interpolation ⋮ Constraint solving for interpolation ⋮ An interpolating sequent calculus for quantifier-free Presburger arithmetic ⋮ An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic ⋮ Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic

Uses Software

• BLAST
• Yices
• FOCI

Cites Work

• Unnamed Item
• Fourier-Motzkin elimination and its dual
• Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
• Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations
• Tools and Algorithms for the Construction and Analysis of Systems
• Automated Deduction – CADE-20
• Constraint Solving for Interpolation
• Efficient Interpolant Generation in Satisfiability Modulo Theories
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Aided Verification

This page was built for publication: Interpolants for Linear Arithmetic in SMT