Interpolation and Symbol Elimination
Kovacs, Laura; Voronkov, Andrei
2009

Abstract

We 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.

Details

Title Interpolation and Symbol Elimination
Author(s) Kovacs, Laura ; Voronkov, Andrei
Published in Automated Deduction - Cade-22
Series Lecture Notes in Computer Science, 5663
Pages 199-213
Conference 22nd International Conference on Automated Deduction (CADE-22), Montreal, CANADA, Aug 02-07, 2009
Date 2009
Publisher Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa
ISBN 978-3-642-02958-5
Keywords
DOI https://doi.org/10.1007/978-3-642-02959-2_17
Other identifier(s) View record in Web of Science
Laboratories MTC
Record Appears in Scientific production and competences > I&C - School of Computer and Communication Sciences > IC Archives > MTC - Models and Theory of Computation Laboratory
Peer-reviewed publications
Conference Papers
Work produced at EPFL
Published
Record creation date 2010-11-30