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 139 articles , 4 standard articles )
Showing results 1 to 20 of 139.
Sorted by year (- Chojecki, Przemysław: Deepalgebra -- an outline of a program (2017)
- Dinsdale-Young, Thomas; da Rocha Pinto, Pedro; Andersen, Kristoffer Just; Birkedal, Lars: Caper - automatic verification for fine-grained concurrency (2017)
- Färber, Michael; Kaliszyk, Cezary; Urban, Josef: Monte Carlo tableau proof search (2017)
- Jakubův, Jan; Urban, Josef: ENIGMA: efficient learning-based inference guiding machine (2017)
- Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark: Constraint solving for finite model finding in SMT solvers (2017)
- 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)
- Brown, Chad E.; Urban, Josef: Extracting higher-order goals from the Mizar Mathematical Library (2016)
- Hoder, Kryštof; Reger, Giles; Suda, Martin; Voronkov, Andrei: Selecting the selection (2016)
- Jakubův, Jan; Urban, Josef: Extending E prover with similarity based clause selection strategies (2016)
- Otten, Jens: Nanocop: a non-clausal connection prover (2016)
- Schulz, Stephan; Möhrmann, Martin: Performance of clause selection heuristics for saturation-based theorem proving (2016)
- Benzmüller, Christoph; Sultana, Nik; Paulson, Lawrence C.; Theiß, Frank: The higher-order prover Leo-II (2015)
- Blanchette, Jasmin Christian; Haslbeck, Maximilian; Matichuk, Daniel; Nipkow, Tobias: Mining the Archive of Formal Proofs (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)
- Färber, Michael; Kaliszyk, Cezary: Random forests for premise selection (2015)
- Kaliszyk, Cezary; Schulz, Stephan; Urban, Josef; Vyskočil, Jiří: System description: E.T. 0.1 (2015)
Further publications can be found at: http://www4.informatik.tu-muenchen.de/~schulz/E/References.html