Kovacs, LauraVoronkov, Andrei2010-11-302010-11-302010-11-30200910.1007/978-3-642-02959-2_17https://infoscience.epfl.ch/handle/20.500.14299/59665WOS:000271347600017We prove several results related to local proofs, interpolation and superposition calculus and discuss their use in predicate abstraction and invariant generation. Our proofs and results suggest that symbol-eliminating inferences may be an interesting alternative to interpolation.Decision ProceduresExtensionsCombinationGenerationTheoremArraysProverInterpolation and Symbol Eliminationtext::conference output::conference proceedings::conference paper