Automated Deduction – CADE-20
From MaRDI portal
Publication:5394624
DOI10.1007/11532231zbMath1135.03331OpenAlexW2485416161MaRDI QIDQ5394624
Madanlal Musuvathi, Greta Yorsh
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
Mechanization of proofs and logical operations (03B35) Interpolation, preservation, definability (03C40)
Related Items
Labelled interpolation systems for hyper-resolution, clausal, and local proofs, Proof tree preserving tree interpolation, Interpolation systems for ground proofs in automated deduction: a survey, 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, Satisfiability Modulo Theories, Interpolation and Model Checking, Modularity results for interpolation, amalgamation and superamalgamation, Constraint solving for interpolation, Complete instantiation-based interpolation, Interpolants for Linear Arithmetic in SMT, Resolution proof transformation for compression and interpolation, On Interpolation in Decision Procedures, Parallelizing SMT solving: lazy decomposition and conciliation, Quantifier-free interpolation in combinations of equality interpolating theories, Rewriting Interpolants, Interpolation and Symbol Elimination in Vampire, Interpolant Generation for UTVPI, Ground Interpolation for Combined Theories, Interpolation and Symbol Elimination, Ground Interpolation for the Theory of Equality, Efficient Interpolant Generation in Satisfiability Modulo Theories, Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic, Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic, Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF, NIL: learning nonlinear interpolants, On invariant synthesis for parametric systems, Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations, Combination of uniform interpolants via Beth definability, Combined covers and Beth definability
Uses Software
