First-Order Theorem Proving and Vampire

By Laura Kovács, Laura Kovács, Andrei Voronkov. 2013

430 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Program Analysis & Verification

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

In Program Analysis & Verification

Citations in the corpus

Solving Quantitative Reasoning Problems with Language Models (2022, neutral): “Work on automation of proof assistants and automated theorem provers such as E [26], leanCoP [27], and Vampire [28] has substantially benefited from integration with machine learning methods [29, 30, 31, 32, 33].”
Premise Selection for Theorem Proving by Deep Graph Embedding (2017, neutral): “Decades of research has resulted in a variety of well-developed automated theorem provers such as Vampire [12] and E [13].”
Monte Carlo Tableau Proof Search (2016, neutral): “…Reasoning include both theoretical improvements in the calculi, including combining superposition with SAT solving in recent versions of Vampire [4] and research on the InstGen calculus in iProver [16], but also more practical improvements, such as more efficient and precise term indexing…”
Deep Network Guided Proof Search (2017, neutral): “Furthermore, the AI methods can be augmented by automated reasoning: progress in the development of eﬃcient ﬁrst-order automated theorem provers (ATPs) (Kovács & Voronkov, 2013) allows applying them not only as tools that redo the formal proofs, but also to ﬁnd the missing steps (Urban, 2006).”
Learning to Prove Theorems via Interacting with Proof Assistants (2019, positive): “More importantly, our model can be combined with state-of-art ATP systems (De Moura & Bjørner, 2008; Barrett et al., 2011; Kov´acs & Voronkov, 2013; Schulz, 2013) and boost the success rate further to 30.0%, which shows that our model has learned effective higher level tactics and has proved new…”
LeanDojo: Theorem Proving with Retrieval-Augmented Language Models (2023, neutral): “Classical provers express theorems in first-order logic and search for proofs automatically in a large space [30, 31].”