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 160 articles , 4 standard articles )

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

1 2 3 ... 6 7 8 next

  1. Alex A. Alemi, Francois Chollet, Niklas Een, Geoffrey Irving, Christian Szegedy, Josef Urban: DeepMath - Deep Sequence Models for Premise Selection (2018) arXiv
  2. Bentkamp, Alexander; Blanchette, Jasmin Christian; Cruanes, Simon; Waldmann, Uwe: Superposition for (\lambda)-free higher-order logic (2018)
  3. Claessen, Koen; Smallbone, Nicholas: Efficient encodings of first-order Horn formulas in equational logic (2018)
  4. Czajka, Łukasz; Kaliszyk, Cezary: Hammer for Coq: automation for dependent type theory (2018)
  5. Echenim, Mnacho; Peltier, Nicolas; Sellami, Yanis: A generic framework for implicate generation modulo theories (2018)
  6. Goertzel, Zarathustra; Jakubův, Jan; Schulz, Stephan; Urban, Josef: Proofwatch: watchlist guidance for large theories in E (2018)
  7. Jakubuv, Jan; Kaliszyk, Cezary: Towards a unified ordering for superposition-based automated reasoning (2018)
  8. Lagniez, Jean-Marie; Le Berre, Daniel; de Lima, Tiago; Montmirail, Valentin: An assumption-based approach for solving the Minimal S5-Satisfiability problem (2018)
  9. Nalon, Cláudia; Pattinson, Dirk: A resolution-based calculus for preferential logics (2018)
  10. Piotrowski, Bartosz; Urban, Josef: ATPboost: learning premise selection in binary setting with ATP feedback (2018)
  11. Schlichtkrull, Anders: Formalization of the resolution calculus for first-order logic (2018)
  12. Winkler, Sarah; Moser, Georg: Mædmax: a maximal ordered completion tool (2018)
  13. Chojecki, Przemysław: Deepalgebra -- an outline of a program (2017)
  14. Dinsdale-Young, Thomas; da Rocha Pinto, Pedro; Andersen, Kristoffer Just; Birkedal, Lars: \textscCaper- automatic verification for fine-grained concurrency (2017)
  15. Färber, Michael; Kaliszyk, Cezary; Urban, Josef: Monte Carlo tableau proof search (2017)
  16. Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef: TacticToe: learning to reason with HOL4 tactics (2017)
  17. Jakubův, Jan; Urban, Josef: ENIGMA: efficient learning-based inference guiding machine (2017)
  18. Kovács, Laura; Robillard, Simon; Voronkov, Andrei: Coming to terms with quantified reasoning (2017)
  19. Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark: Constraint solving for finite model finding in SMT solvers (2017)
  20. Schulz, Stephan; Sutcliffe, Geoff; Urban, Josef; Pease, Adam: Detecting inconsistencies in large first-order knowledge bases (2017)

1 2 3 ... 6 7 8 next


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