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 198 articles , 5 standard articles )

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

1 2 3 ... 8 9 10 next

  1. Bentkamp, Alexander; Blanchette, Jasmin; Cruanes, Simon; Waldmann, Uwe: Superposition for lambda-free higher-order logic (2021)
  2. Bentkamp, Alexander; Blanchette, Jasmin; Tourret, Sophie; Vukmirović, Petar; Waldmann, Uwe: Superposition with lambdas (2021)
  3. Färber, Michael; Kaliszyk, Cezary; Urban, Josef: Machine learning guidance for connection tableaux (2021)
  4. Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef; Kumar, Ramana; Norrish, Michael: TacticToe: learning to prove with tactics (2021)
  5. Steen, Alexander; Benzmüller, Christoph: Extensional higher-order paramodulation in Leo-III (2021)
  6. Barbosa, Haniel; Blanchette, Jasmin Christian; Fleury, Mathias; Fontaine, Pascal: Scalable fine-grained proofs for formula processing (2020)
  7. Baumgartner, Peter; Schmidt, Renate A.: Blocking and other enhancements for bottom-up model generation methods (2020)
  8. Benzmüller, Christoph; Scott, Dana S.: Automating free logic in HOL, with an experimental application in category theory (2020)
  9. Berghammer, Rudolf; Furusawa, Hitoshi; Guttmann, Walter; Höfner, Peter: Relational characterisations of paths (2020)
  10. Confalonieri, Roberto; Kutz, Oliver: Blending under deconstruction. The roles of logic, ontology, and cognition in computational concept invention (2020)
  11. Diaconescu, Răzvan: Introducing (H), an institution-based formal specification and verification language (2020)
  12. Echenim, M.; Peltier, N.: Combining induction and saturation-based theorem proving (2020)
  13. Jakubův, Jan; Kaliszyk, Cezary: Relaxed weighted path order in theorem proving (2020)
  14. Luigi Bellomarini, Georg Gottlob, Emanuel Sallinger: The Vadalog System: Datalog-based Reasoning for Knowledge Graphs (2020) arXiv
  15. Barbosa, Haniel; Reynolds, Andrew; El Ouraoui, Daniel; Tinelli, Cesare; Barrett, Clark: Extending SMT solvers to higher-order logic (2019)
  16. Bentkamp, Alexander; Blanchette, Jasmin; Tourret, Sophie; Vukmirović, Petar; Waldmann, Uwe: Superposition with lambdas (2019)
  17. Bhayat, Ahmed; Reger, Giles: Restricted combinatory unification (2019)
  18. Brown, Chad E.; Gauthier, Thibault; Kaliszyk, Cezary; Sutcliffe, Geoff; Urban, Josef: GRUNGE: a grand unified ATP challenge (2019)
  19. Chvalovský, Karel; Jakubův, Jan; Suda, Martin; Urban, Josef: ENIGMA-NG: efficient neural and gradient-boosted inference guidance for (\mathrmE) (2019)
  20. Ebner, Gabriel: Herbrand constructivization for automated intuitionistic theorem proving (2019)

1 2 3 ... 8 9 10 next


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