conference paper
Interpolation and Symbol Elimination
Kovacs, Laura
•
Voronkov, Andrei
2009
Automated Deduction - Cade-22
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.
Type
conference paper
Web of Science ID
WOS:000271347600017
Author(s)
Kovacs, Laura
Voronkov, Andrei
Date Issued
2009
Published in
Automated Deduction - Cade-22
ISBN of the book
978-3-642-02958-5
Series title/Series vol.
Lecture Notes in Computer Science; 5663
Start page
199
End page
213
Subjects
Editorial or Peer reviewed
REVIEWED
Written at
EPFL
EPFL units
| Event name | Event place | Event date |
Montreal, CANADA | Aug 02-07, 2009 | |
Available on Infoscience
November 30, 2010
Use this identifier to reference this record