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 207 articles , 5 standard articles )
Showing results 1 to 20 of 207.
Sorted by year (- Bentkamp, Alexander; Blanchette, Jasmin; Cruanes, Simon; Waldmann, Uwe: Superposition for lambda-free higher-order logic (2021)
- Bentkamp, Alexander; Blanchette, Jasmin; Tourret, Sophie; Vukmirović, Petar; Waldmann, Uwe: Superposition with lambdas (2021)
- Chvalovský, Karel; Jakubův, Jan; Olšák, Miroslav; Urban, Josef: Learning theorem proving components (2021)
- Duarte, André; Korovin, Konstantin: AC simplifications and closure redundancies in the superposition calculus (2021)
- Färber, Michael; Kaliszyk, Cezary; Urban, Josef: Machine learning guidance for connection tableaux (2021)
- Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef; Kumar, Ramana; Norrish, Michael: TacticToe: learning to prove with tactics (2021)
- Goertzel, Zarathustra A.; Chvalovský, Karel; Jakubův, Jan; Olšák, Miroslav; Urban, Josef: Fast and slow enigmas and parental guidance (2021)
- Holden, Edvard K.; Korovin, Konstantin: Heterogeneous heuristic optimisation and scheduling for first-order theorem proving (2021)
- Rawson, Michael; Reger, Giles: \textsflazyCoP: lazy paramodulation meets neurally guided search (2021)
- Schurr, Hans-Jörg; Fleury, Mathias; Desharnais, Martin: Reliable reconstruction of fine-grained proofs in a proof assistant (2021)
- Steen, Alexander; Benzmüller, Christoph: Extensional higher-order paramodulation in Leo-III (2021)
- Sutcliffe, Geoff: The 10th IJCAR automated theorem proving system competition -- CASC-J10 (2021)
- Zombori, Zsolt; Csiszárik, Adrián; Michalewski, Henryk; Kaliszyk, Cezary; Urban, Josef: Towards finding longer proofs (2021)
- Zombori, Zsolt; Urban, Josef; Olšák, Miroslav: The role of entropy in guiding a connection prover (2021)
- 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)
- Berghammer, Rudolf; Furusawa, Hitoshi; Guttmann, Walter; Höfner, Peter: Relational characterisations of paths (2020)
- Confalonieri, Roberto; Kutz, Oliver: Blending under deconstruction. The roles of logic, ontology, and cognition in computational concept invention (2020)
- Diaconescu, Răzvan: Introducing (H), an institution-based formal specification and verification language (2020)
Further publications can be found at: http://www4.informatik.tu-muenchen.de/~schulz/E/References.html