E 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 112 articles , 3 standard articles )
Showing results 1 to 20 of 112.
Sorted by year (- Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
- Blanchette, Jasmin Christian; Böhme, Sascha; Popescu, Andrei; Smallbone, Nicholas: Encoding monomorphic and polymorphic types (2016)
- Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef: A learning-based fact selector for Isabelle/HOL (2016)
- Bonacina, Maria Paola; Plaisted, David A.: Semantically-guided goal-sensitive reasoning: model representation (2016)
- Jakubův, Jan; Urban, Josef: Extending E prover with similarity based clause selection strategies (2016)
- Benzmüller, Christoph; Sultana, Nik; Paulson, Lawrence C.; Theiß, Frank: The higher-order prover Leo-II (2015)
- Bonacina, Maria Paola; Johansson, Moa: On interpolation in automated theorem proving (2015)
- Echenim, Mnacho; Peltier, Nicolas; Tourret, Sophie: Quantifier-free equational logic and prime implicate generation (2015)
- Kaliszyk, Cezary; Schulz, Stephan; Urban, Josef; Vyskočil, Jiří: System description: E.T. 0.1 (2015)
- Kaliszyk, Cezary; Urban, Josef: MizAR 40 for Mizar 40 (2015)
- Kaliszyk, Cezary; Urban, Josef: HOL(y)Hammer: online ATP service for HOL Light (2015)
- Kaliszyk, Cezary; Urban, Josef: Learning-assisted theorem proving with millions of lemmas (2015)
- Kühlwein, Daniel; Urban, Josef: MaLeS: a framework for automatic tuning of automated theorem provers (2015)
- Plaisted, David A.: History and prospects for first-order automated deduction (2015)
- Reger, Giles; Tishkovsky, Dmitry; Voronkov, Andrei: Cooperating proof attempts (2015)
- Stojanović {\Dj}urđević, Sana; Narboux, Julien; Janičić, Predrag: Automated generation of machine verifiable and readable proofs: a case study of Tarski’s geometry (2015)
- Alama, Jesse; Heskes, Tom; Kühlwein, Daniel; Tsivtsivadze, Evgeni; Urban, Josef: Premise selection for mathematics by corpus analysis and kernel methods (2014)
- Bridge, James P.; Holden, Sean B.; Paulson, Lawrence C.: Machine learning for first-order theorem proving (2014)
- James, Phillip; Roggenbach, Markus: Encapsulating formal methods within domain specific languages: a solution for verifying railway scheme plans (2014)
- Kaliszyk, Cezary; Urban, Josef: Learning-assisted automated reasoning with $\mathsfFlyspeck$ (2014)
Further publications can be found at: http://www4.informatik.tu-muenchen.de/~schulz/E/References.html