Interpolation and Symbol Elimination

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.


Published in:
Automated Deduction - Cade-22, 5663, 199-213
Presented at:
22nd International Conference on Automated Deduction (CADE-22), Montreal, CANADA, Aug 02-07, 2009
Year:
2009
Publisher:
Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa
ISBN:
978-3-642-02958-5
Keywords:
Laboratories:




 Record created 2010-11-30, last modified 2018-03-17


Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)