Interpolation in local theory extensions
From MaRDI portal
Publication:3622999
DOI10.2168/LMCS-4(4:1)2008zbMath1170.03018MaRDI QIDQ3622999
Publication date: 29 April 2009
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
68T30: Knowledge representation
68Q60: Specification and verification (program logics, model checking, etc.)
03B35: Mechanization of proofs and logical operations
03C40: Interpolation, preservation, definability
Related Items
SMT-based verification of data-aware processes: a model-theoretic approach, Complete instantiation-based interpolation, Interpolation Results for Arrays with Length and MaxDiff, Interpolation systems for ground proofs in automated deduction: a survey, Constraint solving for interpolation, Interpolation and amalgamation for arrays with MaxDiff, On invariant synthesis for parametric systems, Modularity results for interpolation, amalgamation and superamalgamation, Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF, On Interpolation and Symbol Elimination in Theory Extensions, On First-Order Model-Based Reasoning