Abstract
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. © 2010 Springer-Verlag.
Cite
CITATION STYLE
Hoder, K., Kovács, L., & Voronkov, A. (2010). Interpolation and symbol elimination in vampire. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6173 LNAI, pp. 188–195). https://doi.org/10.1007/978-3-642-14203-1_16
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
