E Theorem Prover

E: A Brainiac 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 138 articles , 4 standard articles )

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

1 2 3 ... 5 6 7 next

  1. Chojecki, Przemysław: Deepalgebra -- an outline of a program (2017)
  2. Dinsdale-Young, Thomas; da Rocha Pinto, Pedro; Andersen, Kristoffer Just; Birkedal, Lars: Caper - automatic verification for fine-grained concurrency (2017)
  3. Färber, Michael; Kaliszyk, Cezary; Urban, Josef: Monte Carlo tableau proof search (2017)
  4. Jakubův, Jan; Urban, Josef: ENIGMA: efficient learning-based inference guiding machine (2017)
  5. Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
  6. Blanchette, Jasmin Christian; Böhme, Sascha; Popescu, Andrei; Smallbone, Nicholas: Encoding monomorphic and polymorphic types (2016)
  7. Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef: A learning-based fact selector for Isabelle/HOL (2016)
  8. Bonacina, Maria Paola; Plaisted, David A.: Semantically-guided goal-sensitive reasoning: model representation (2016)
  9. Brown, Chad E.; Urban, Josef: Extracting higher-order goals from the Mizar Mathematical Library (2016)
  10. Hoder, Kryštof; Reger, Giles; Suda, Martin; Voronkov, Andrei: Selecting the selection (2016)
  11. Jakubův, Jan; Urban, Josef: Extending E prover with similarity based clause selection strategies (2016)
  12. Otten, Jens: Nanocop: a non-clausal connection prover (2016)
  13. Schulz, Stephan; Möhrmann, Martin: Performance of clause selection heuristics for saturation-based theorem proving (2016)
  14. Benzmüller, Christoph; Sultana, Nik; Paulson, Lawrence C.; Theiß, Frank: The higher-order prover Leo-II (2015)
  15. Blanchette, Jasmin Christian; Haslbeck, Maximilian; Matichuk, Daniel; Nipkow, Tobias: Mining the Archive of Formal Proofs (2015)
  16. Bonacina, Maria Paola; Johansson, Moa: On interpolation in automated theorem proving (2015)
  17. Echenim, Mnacho; Peltier, Nicolas; Tourret, Sophie: Quantifier-free equational logic and prime implicate generation (2015)
  18. Färber, Michael; Kaliszyk, Cezary: Random forests for premise selection (2015)
  19. Kaliszyk, Cezary; Schulz, Stephan; Urban, Josef; Vyskočil, Jiří: System description: E.T. 0.1 (2015)
  20. Kaliszyk, Cezary; Urban, Josef: Learning-assisted theorem proving with millions of lemmas (2015)

1 2 3 ... 5 6 7 next


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