Automated Deduction – CADE-20
From MaRDI portal
Publication:5394624
DOI10.1007/11532231zbMath1135.03331MaRDI QIDQ5394624
Greta Yorsh, Madanlal Musuvathi
Publication date: 1 November 2006
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/11532231
03B35: Mechanization of proofs and logical operations
03C40: Interpolation, preservation, definability
Related Items
Interpolant Generation for UTVPI, Ground Interpolation for Combined Theories, Interpolation and Symbol Elimination, Efficient Interpolant Generation in Satisfiability Modulo Theories, Interpolation and Symbol Elimination in Vampire, Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic, Constraint solving for interpolation, Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations, On Interpolation in Decision Procedures, Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic, Craig Interpolation in the Presence of Non-linear Constraints, A Combination of Rewriting and Constraint Solving for the Quantifier-Free Interpolation of Arrays with Integer Difference Constraints, Interpolants for Linear Arithmetic in SMT, Ground Interpolation for the Theory of Equality
Uses Software
