E Theorem Prover

E is a theorem prover for full first-order logic with equality. It accepts a problem specification, typically consisting of a number of first-order clauses or formulas, and a conjecture, again either in clausal or full first-order form. The system will then try to find a formal proof for the conjecture, assuming the axioms. If a proof is found, the system can provide a detailed list of proof steps that can be individually verified. If the conjecture is existential (i.e. it’s of the form “there exists an X with property P”), the latest versions can also provide possible answers (values for X). Development of E started as part of the E-SETHEO project at TUM. The first public release was in in 1998, and the system has been continuously improved ever since. I believe that E now is one of the most powerful and friendly reasoning systems for first-order logic. The prover has successfully participated in many competitions.


References in zbMATH (referenced in 114 articles , 3 standard articles )

Showing results 1 to 20 of 114.
Sorted by year (citations)

1 2 3 4 5 6 next

  1. Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
  2. Blanchette, Jasmin Christian; Böhme, Sascha; Popescu, Andrei; Smallbone, Nicholas: Encoding monomorphic and polymorphic types (2016)
  3. Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef: A learning-based fact selector for Isabelle/HOL (2016)
  4. Bonacina, Maria Paola; Plaisted, David A.: Semantically-guided goal-sensitive reasoning: model representation (2016)
  5. Jakubův, Jan; Urban, Josef: Extending E prover with similarity based clause selection strategies (2016)
  6. Benzmüller, Christoph; Sultana, Nik; Paulson, Lawrence C.; Theiß, Frank: The higher-order prover Leo-II (2015)
  7. Bonacina, Maria Paola; Johansson, Moa: On interpolation in automated theorem proving (2015)
  8. Echenim, Mnacho; Peltier, Nicolas; Tourret, Sophie: Quantifier-free equational logic and prime implicate generation (2015)
  9. Kaliszyk, Cezary; Schulz, Stephan; Urban, Josef; Vyskočil, Jiří: System description: E.T. 0.1 (2015)
  10. Kaliszyk, Cezary; Urban, Josef: HOL(y)Hammer: online ATP service for HOL Light (2015)
  11. Kaliszyk, Cezary; Urban, Josef: MizAR 40 for Mizar 40 (2015)
  12. Kaliszyk, Cezary; Urban, Josef: Learning-assisted theorem proving with millions of lemmas (2015)
  13. Kühlwein, Daniel; Urban, Josef: MaLeS: a framework for automatic tuning of automated theorem provers (2015)
  14. Plaisted, David A.: History and prospects for first-order automated deduction (2015)
  15. Reger, Giles; Tishkovsky, Dmitry; Voronkov, Andrei: Cooperating proof attempts (2015)
  16. Stojanović {\Dj}urđević, Sana; Narboux, Julien; Janičić, Predrag: Automated generation of machine verifiable and readable proofs: a case study of Tarski’s geometry (2015)
  17. Alama, Jesse; Heskes, Tom; Kühlwein, Daniel; Tsivtsivadze, Evgeni; Urban, Josef: Premise selection for mathematics by corpus analysis and kernel methods (2014)
  18. Bridge, James P.; Holden, Sean B.; Paulson, Lawrence C.: Machine learning for first-order theorem proving (2014)
  19. James, Phillip; Roggenbach, Markus: Encapsulating formal methods within domain specific languages: a solution for verifying railway scheme plans (2014)
  20. Kaliszyk, Cezary; Urban, Josef: Learning-assisted automated reasoning with $\mathsfFlyspeck$ (2014)

1 2 3 4 5 6 next


Further publications can be found at: http://www4.informatik.tu-muenchen.de/~schulz/E/References.html