Interpolation and Symbol Elimination in Vampire

It has recently been shown that proofs in which some symbols are colored (e.g. local or split proofs and symbol-eliminating proofs) can be used for a number of applications, such as invariant generation and computing interpolants. This tool paper describes how such proofs and interpolant generation are implemented in the first-order theorem prover Vampire.

• Type: Conference
• Year: 2010
• Where: CADE
• Authors: Krystof Hoder, Laura Kovács, Andrei Voronkov
• Keywords: CADE 2010, First-order Theorem Prover, Logical Reasoning, Split Proofs, Symbol-eliminating Proofs