E Theorem Prover swMATH ID: 10187 Software Authors: Stephan Schulz Description: 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. Homepage: http://www4.informatik.tu-muenchen.de/~schulz/E/E.html Related Software: VAMPIRE; TPTP; SPASS; Isabelle/HOL; Mizar; Sledgehammer; z3; MaLARea; HOL Light; OTTER; HOL; MPTP 0.2; Satallax; Metis_; Coq; Flyspeck; Mace4; LEO-II; MaLeCoP; Isabelle Cited in: 214 Publications Further Publications: http://www4.informatik.tu-muenchen.de/~schulz/E/References.html Standard Articles 5 Publications describing the Software, including 5 Publications in zbMATH Year Faster, higher, stronger: E 2.3. Zbl 07178994Schulz, Stephan; Cruanes, Simon; Vukmirović, Petar 2019 System description: E 1.8. Zbl 1407.68442Schulz, Stephan 2013 System description: E 0.81. Zbl 1126.68578Schulz, Stephan 2004 E – a brainiac theorem prover. Zbl 1020.68084Schulz, Stephan 2002 System abstract: E 0. 61. Zbl 0988.68602Schulz, Stephan 2001 all top 5 Cited by 244 Authors 46 Urban, Josef 20 Kaliszyk, Cezary 19 Schulz, Stephan 18 Sutcliffe, Geoff 15 Blanchette, Jasmin Christian 13 Paulson, Lawrence Charles 12 Benzmüller, Christoph Ewald 12 Voronkov, Andrei 10 Jakubův, Jan 8 Hustadt, Ullrich 8 Ranise, Silvio 8 Reger, Giles 7 Bonacina, Maria Paola 7 Schmidt, Renate A. 6 Kühlwein, Daniel 6 Waldmann, Uwe 5 Baumgartner, Peter 5 Böhme, Sascha 5 Chvalovský, Karel 5 Claessen, Koen 5 Cruanes, Simon 5 Korovin, Konstantin 5 Nipkow, Tobias 5 Peltier, Nicolas 5 Tinelli, Cesare 5 Vyskočil, Jiří 4 Bentkamp, Alexander 4 Brown, Chad Edward 4 Echenim, Mnacho 4 Kovács, Laura Ildikó 4 Nalon, Cláudia 4 Olšák, Miroslav 4 Tourret, Sophie 4 Vukmirović, Petar 3 Armando, Alessandro 3 Bozzano, Marco 3 Bruttomesso, Roberto 3 Cimatti, Alessandro 3 Dixon, Clare 3 Duarte, André 3 Färber, Michael 3 Fleury, Mathias 3 Gauthier, Thibault 3 Heskes, Tom M. 3 Hoder, Kryštof 3 Junttila, Tommi A. 3 Pease, Adam 3 Plaisted, David Alan 3 Rawson, Michael 3 Sebastiani, Roberto 3 Suda, Martin 3 Sultana, Nik 3 Theiss, Frank 3 Tishkovsky, Dmitry 3 Tran, Duc-Khanh 3 van Rossum, Peter 3 Zombori, Zsolt 2 Alama, Jesse 2 Barbosa, Haniel 2 Barrett, Clark W. 2 Bensaid, Hicham 2 Bhayat, Ahmed 2 Caferra, Ricardo 2 Colton, Simon 2 Déharbe, David 2 Endriss, Ulle 2 Fontaine, Pascal 2 Furbach, Ulrich 2 Goertzel, Zarathustra Amadeus 2 Grandi, Umberto 2 Höfner, Peter 2 Janičić, Predrag 2 Koepke, Peter 2 Lillieström, Ann 2 Löchner, Bernd 2 Lyaletski, Alexander V. 2 McCasland, Roy L. 2 Meier, Andreas 2 Meng, Jia 2 Motik, Boris 2 Papacchini, Fabio 2 Pelzer, Björn 2 Piotrowski, Bartosz 2 Puzis, Yury 2 Reynolds, Andrew 2 Riazanov, Alexandre 2 Ringeissen, Christophe 2 Robillard, Simon 2 Smallbone, Nicholas 2 Sorge, Volker 2 Stanovský, David 2 Stojanović Đurđević, Sana 2 Trac, Steven 2 Tsivtsivadze, Evgeni 2 Verchinine, Konstantin 2 Weidenbach, Christoph 2 Wenzel, Makarius 2 Woltzenlogel Paleo, Bruno 1 Andersen, Kristoffer Just Arndal 1 Bancerek, Grzegorz ...and 144 more Authors all top 5 Cited in 25 Serials 32 Journal of Automated Reasoning 8 AI Communications 7 Annals of Mathematics and Artificial Intelligence 5 Journal of Applied Logic 4 Mathematics in Computer Science 3 Information and Computation 3 ACM Transactions on Computational Logic 2 Artificial Intelligence 2 Journal of Symbolic Computation 2 Lecture Notes in Computer Science 2 Logical Methods in Computer Science 2 Journal of Formalized Reasoning 1 Commentationes Mathematicae Universitatis Carolinae 1 Fuzzy Sets and Systems 1 Information Sciences 1 Journal of Philosophical Logic 1 Formal Aspects of Computing 1 MSCS. Mathematical Structures in Computer Science 1 Cybernetics and Systems Analysis 1 Logic Journal of the IGPL 1 Theory and Practice of Logic Programming 1 Logica Universalis 1 Journal of Logical and Algebraic Methods in Programming 1 DISKI. Dissertationen zur Künstlichen Intelligenz 1 Philosophical Transactions of the Royal Society of London. A. Mathematical, Physical and Engineering Sciences all top 5 Cited in 11 Fields 206 Computer science (68-XX) 77 Mathematical logic and foundations (03-XX) 2 General and overarching topics; collections (00-XX) 2 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 1 History and biography (01-XX) 1 Combinatorics (05-XX) 1 Commutative algebra (13-XX) 1 Algebraic geometry (14-XX) 1 Category theory; homological algebra (18-XX) 1 Group theory and generalizations (20-XX) 1 Geometry (51-XX) Citations by Year