E-SETHEO: An automated3 theorem prover We have developed a method for strategy evaluation and selection based on test data generated from the problem domain. We present the theorem prover e-SETHEO, which automatically handles training data management, strategy evaluation and selection, and actual proof tasks. We also give some experimental data produced with this system. We address the problem of test set extraction and give an assessment of our work.

References in zbMATH (referenced in 15 articles )

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

  1. Kaliszyk, Cezary: Efficient low-level connection tableaux (2015)
  2. Kühlwein, Daniel; Schulz, Stephan; Urban, Josef: E-MaLeS 1.1 (2013)
  3. Björk, Magnus: First order St\aalmarck. Universal lemmas through branch merges (2009)
  4. Jürjens, Jan: Automated security verification for crypto protocol implementations: verifying the jessie project (2009)
  5. Jürjens, Jan: A domain-specific language for cryptographic protocols based on streams (2009)
  6. Benzmüller, Christoph; Sorge, Volker; Jamnik, Mateja; Kerber, Manfred: Combined reasoning by automated cooperation (2008)
  7. Paskevich, Andrei: Connection tableaux with lazy paramodulation (2008)
  8. Letz, Reinhold; Stenz, Gernot: The disconnection tableau calculus (2007)
  9. Benzmüller, Christoph; Sorge, Volker; Jamnik, Mateja; Kerber, Manfred: Can a higher-order and a first-order theorem prover cooperate? (2005)
  10. Otten, Jens; Bibel, Wolfgang: IeanCOP: lean connection-based theorem proving (2003)
  11. Riazanov, Alexandre; Voronkov, Andrei: Limited resource strategy in resolution theorem proving (2003)
  12. Fuchs, Marc: Controlled use of clausal lemmas in connection tableau calculi (2000)
  13. Stenz, Gernot; Wolf, Andreas: E-SETHEO: An automated$^3$ theorem prover (2000)
  14. Bibel, W.: Let’s plan it deductively! (1998)
  15. Moser, Max; Ibens, Ortrun; Letz, Reinhold; Steinbach, Joachim; Goller, Christoph; Schumann, Johann; Mayr, Klaus: The CADE-13 systems SETHEO and E-SETHEO. (1997)