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.


References in zbMATH (referenced in 207 articles , 5 standard articles )

Showing results 1 to 20 of 207.
Sorted by year (citations)

1 2 3 ... 9 10 11 next

  1. Bentkamp, Alexander; Blanchette, Jasmin; Cruanes, Simon; Waldmann, Uwe: Superposition for lambda-free higher-order logic (2021)
  2. Bentkamp, Alexander; Blanchette, Jasmin; Tourret, Sophie; Vukmirović, Petar; Waldmann, Uwe: Superposition with lambdas (2021)
  3. Chvalovský, Karel; Jakubův, Jan; Olšák, Miroslav; Urban, Josef: Learning theorem proving components (2021)
  4. Duarte, André; Korovin, Konstantin: AC simplifications and closure redundancies in the superposition calculus (2021)
  5. Färber, Michael; Kaliszyk, Cezary; Urban, Josef: Machine learning guidance for connection tableaux (2021)
  6. Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef; Kumar, Ramana; Norrish, Michael: TacticToe: learning to prove with tactics (2021)
  7. Goertzel, Zarathustra A.; Chvalovský, Karel; Jakubův, Jan; Olšák, Miroslav; Urban, Josef: Fast and slow enigmas and parental guidance (2021)
  8. Holden, Edvard K.; Korovin, Konstantin: Heterogeneous heuristic optimisation and scheduling for first-order theorem proving (2021)
  9. Rawson, Michael; Reger, Giles: \textsflazyCoP: lazy paramodulation meets neurally guided search (2021)
  10. Schurr, Hans-Jörg; Fleury, Mathias; Desharnais, Martin: Reliable reconstruction of fine-grained proofs in a proof assistant (2021)
  11. Steen, Alexander; Benzmüller, Christoph: Extensional higher-order paramodulation in Leo-III (2021)
  12. Sutcliffe, Geoff: The 10th IJCAR automated theorem proving system competition -- CASC-J10 (2021)
  13. Zombori, Zsolt; Csiszárik, Adrián; Michalewski, Henryk; Kaliszyk, Cezary; Urban, Josef: Towards finding longer proofs (2021)
  14. Zombori, Zsolt; Urban, Josef; Olšák, Miroslav: The role of entropy in guiding a connection prover (2021)
  15. Barbosa, Haniel; Blanchette, Jasmin Christian; Fleury, Mathias; Fontaine, Pascal: Scalable fine-grained proofs for formula processing (2020)
  16. Baumgartner, Peter; Schmidt, Renate A.: Blocking and other enhancements for bottom-up model generation methods (2020)
  17. Benzmüller, Christoph; Scott, Dana S.: Automating free logic in HOL, with an experimental application in category theory (2020)
  18. Berghammer, Rudolf; Furusawa, Hitoshi; Guttmann, Walter; Höfner, Peter: Relational characterisations of paths (2020)
  19. Confalonieri, Roberto; Kutz, Oliver: Blending under deconstruction. The roles of logic, ontology, and cognition in computational concept invention (2020)
  20. Diaconescu, Răzvan: Introducing (H), an institution-based formal specification and verification language (2020)

1 2 3 ... 9 10 11 next


Further publications can be found at: http://www4.informatik.tu-muenchen.de/~schulz/E/References.html