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.
Keywords for this software
References in zbMATH (referenced in 181 articles , 5 standard articles )
Showing results 1 to 20 of 181.
Sorted by year (- Barbosa, Haniel; Blanchette, Jasmin Christian; Fleury, Mathias; Fontaine, Pascal: Scalable fine-grained proofs for formula processing (2020)
- Baumgartner, Peter; Schmidt, Renate A.: Blocking and other enhancements for bottom-up model generation methods (2020)
- Benzmüller, Christoph; Scott, Dana S.: Automating free logic in HOL, with an experimental application in category theory (2020)
- Echenim, M.; Peltier, N.: Combining induction and saturation-based theorem proving (2020)
- Barbosa, Haniel; Reynolds, Andrew; El Ouraoui, Daniel; Tinelli, Cesare; Barrett, Clark: Extending SMT solvers to higher-order logic (2019)
- Bentkamp, Alexander; Blanchette, Jasmin; Tourret, Sophie; Vukmirović, Petar; Waldmann, Uwe: Superposition with lambdas (2019)
- Bhayat, Ahmed; Reger, Giles: Restricted combinatory unification (2019)
- Brown, Chad E.; Gauthier, Thibault; Kaliszyk, Cezary; Sutcliffe, Geoff; Urban, Josef: GRUNGE: a grand unified ATP challenge (2019)
- Chvalovský, Karel; Jakubův, Jan; Suda, Martin; Urban, Josef: ENIGMA-NG: efficient neural and gradient-boosted inference guidance for (\mathrmE) (2019)
- Furbach, Ulrich; Krämer, Teresa; Schon, Claudia: Names are not just sound and smoke: word embeddings for axiom selection (2019)
- Mohamed Yacine El Haddad, Guillaume Burel, Frédéric Blanqui: EKSTRAKTO A tool to reconstruct Dedukti proofs from TSTP files (extended abstract) (2019) arXiv
- Nikolić, Mladen; Marinković, Vesna; Kovács, Zoltán; Janičić, Predrag: Portfolio theorem proving and prover runtime prediction for geometry (2019)
- Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius: From LCF to Isabelle/HOL (2019)
- Rawson, Michael; Reger, Giles: Old or heavy? Decaying gracefully with age/weight shapes (2019)
- Reger, Giles; Voronkov, Andrei: Induction in saturation-based proof search (2019)
- Reis, Giselle; Woltzenlogel Paleo, Bruno: Complexity of translations from resolution to sequent calculus (2019)
- Schulz, Stephan; Cruanes, Simon; Vukmirović, Petar: Faster, higher, stronger: E 2.3 (2019)
- Stojanović-Ðurđević, Sana: From informal to formal proofs in Euclidean geometry (2019)
- Alex A. Alemi, Francois Chollet, Niklas Een, Geoffrey Irving, Christian Szegedy, Josef Urban: DeepMath - Deep Sequence Models for Premise Selection (2018) arXiv
- Bentkamp, Alexander; Blanchette, Jasmin Christian; Cruanes, Simon; Waldmann, Uwe: Superposition for (\lambda)-free higher-order logic (2018)
Further publications can be found at: http://www4.informatik.tu-muenchen.de/~schulz/E/References.html