System Description: E 1.8

By S. Schulz. 2013

258 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Natural Language Processing, 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 Natural Language Processing

In Program Analysis & Verification

Citations in the corpus

Solving Quantitative Reasoning Problems with Language Models (2022, background): “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].”
Reinforcement Learning of Theorem Proving (2018, methodology): “The Miz40 dataset was created [21] by running state-of-the-art first-order ATPs - mainly E [40] and Vampire [26] - on various axiom selections in many different ways, followed by pseudominimization [1] of the set of axioms.”
Monte Carlo Tableau Proof Search (2016, methodology): “…advances in Automated 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…”
Deep Network Guided Proof Search (2017, methodology): “Although all the hard statements have human proofs, this subset could neither be proved by theorem prover E (Schulz, 2013) nor by Vampire (Kovács & Voronkov, 2013) with a timeout limit of 15 minutes and default settings (auto and casc heuristics respectively) using the premises derived from the…”
Learning to Prove Theorems via Interacting with Proof Assistants (2019, methodology): “Automated theorem proving Modern theorem provers (Kov ´ acs & Voronkov, 2013; Schulz, 2013) represent theorems in ﬁrst-order logic and search for proofs in resolution-based proof calculi.”
Improving Graph Neural Network Representations of Logical Formulae with Subgraph Pooling (2019, methodology): “We also demonstrate how to easily integrate our approach with E, a well-established theorem prover [26], as its premise selection mechanism, allowing it to find more proofs (61.”
INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving (2020, unknown): “Automatic Theorem Proving Modern Automatic Theorem Provers (ATPs) such as E [26] and Vampire [18] represent mathematical theorems in ﬁrst-order logic and prove them with resolution-based proof calculi.”