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)
Knowledge representation (68T30) Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Interpolation, preservation, definability (03C40)
Related Items (11)
Interpolation systems for ground proofs in automated deduction: a survey ⋮ Modularity results for interpolation, amalgamation and superamalgamation ⋮ Constraint solving for interpolation ⋮ On First-Order Model-Based Reasoning ⋮ Interpolation Results for Arrays with Length and MaxDiff ⋮ Complete instantiation-based interpolation ⋮ SMT-based verification of data-aware processes: a model-theoretic approach ⋮ Interpolation and amalgamation for arrays with MaxDiff ⋮ Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF ⋮ On Interpolation and Symbol Elimination in Theory Extensions ⋮ On invariant synthesis for parametric systems
This page was built for publication: Interpolation in local theory extensions
