Interpolation and Symbol Elimination

Abstract. We prove several results related to local proofs, interpolation and suion 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.

• Type: Conference
• Year: 2009
• Where: CADE
• Authors: Andrei Voronkov, Laura Kovács
• Keywords: Automated Reasoning, CADE 2009, Invariant Generation, Local Proofs, Predicate Abstraction