E – a brainiac theorem prover

By S. Schulz. AI Communications, 2002

568 citations recorded by the source corpus.

View Paper: https://www.semanticscholar.org/paper/7cabc21f57b5df93534151df4cc5d09e64db2ad6

How researchers see this paper

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

1. Yoshua Bengio
2. Jia Deng
3. Quoc V. Le
4. Sergey Levine
5. Trevor Darrell
6. Ruslan Salakhutdinov
7. Mohit Bansal
8. Dacheng Tao

Citations in the corpus

• Monte Carlo Tableau Proof Search (2016, methodology): “This heuristic is based on similar ideas as the pick-given ratio popularised by Otter [23].”
• HyperTree Proof Search for Neural Theorem Proving (2022, background): “Early approaches focused on simpler logics, culminating in extremely efficient first-order provers such as E [11] or Vampire [12].”
• GamePad: A Learning Environment for Theorem Proving (2018, methodology): “[6] describes the premise selection problem and trains neural network models on proof traces obtained from applying E [19] to the Mizar Mathematical Corpus.”
• History of Interactive Theorem Proving (2014, methodology): “…Bridge, Kaliszyk, Kühlwein and others have recently used machine learning for selecting suitable theorem-proving strategies [Kühlwein et al., 2013; Schulz, 2002; Bridge et al., 2014] and automated construction of such strategies [Urban, 2014] over large sets of related problems, mining the…”
• Premise Selection for Theorem Proving by Deep Graph Embedding (2017, background): “Decades of research has resulted in a variety of well-developed automated theorem provers such as Vampire [12] and E [13].”
• Learning to Prove Theorems by Learning to Generate Theorems (2020, background): “Loos et al. (2017) proposes to learn clause selection by deep learning inside the first-order logic prover E (Schulz, 2002).”
• Solving olympiad geometry without human demonstrations (2024, unknown): “44) or Vampire 45 .”
• The TPTP Problem Library and Associated Infrastructure (2009, methodology): “A proposal for this language has been established, and a prototype implementation is underway in the E ATP system [34].”
• HOList: An Environment for Machine Learning of Higher-Order Theorem Proving (extended version) (2019, methodology): “Those methods were used as a pre-selection for applying the first order logic automated theorem prover E [20].”
• DeepMath - Deep Sequence Models for Premise Selection (2016, background): “11473 as the formal corpus and E prover [32] version 1.”