Skip to main content
Conference ProceedingsOPEN ACCESS

First-order theorem proving and VAMPIRE

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (2013) 8044 LNCS 1-35
DOI: 10.1007/978-3-642-39799-8_1
370Citations
Citations of this article
58Readers
Mendeley users who have this article in their library.

This article is free to access.

Abstract

In this paper we give a short introduction in first-order theorem proving and the use of the theorem prover Vampire. We discuss the superposition calculus and explain the key concepts of saturation and redundancy elimination, present saturation algorithms and preprocessing, and demonstrate how these concepts are implemented in Vampire. Further, we also cover more recent topics and features of Vampire designed for advanced applications, including satisfiability checking, theory reasoning, interpolation, consequence elimination, and program analysis. © 2013 Springer-Verlag.

Cite

CITATION STYLE

APA

Kovács, L., & Voronkov, A. (2013). First-order theorem proving and VAMPIRE. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8044 LNCS, pp. 1–35). https://doi.org/10.1007/978-3-642-39799-8_1

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free