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.
Viktor Kuncak, Simon Guilloud, Sankalp Gambhir
Viktor Kuncak, Simon Guilloud, Sankalp Gambhir
Maryna Viazovska, Abhinav Kumar