E-SETHEO

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 17 articles )

Showing results 1 to 17 of 17.
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ålmarck. Universal lemmas through branch merges (2009)
  4. Jürjens, Jan: A domain-specific language for cryptographic protocols based on streams (2009)
  5. Benzmüller, Christoph; Sorge, Volker; Jamnik, Mateja; Kerber, Manfred: Combined reasoning by automated cooperation (2008)
  6. Paskevich, Andrei: Connection tableaux with lazy paramodulation (2008)
  7. Letz, Reinhold; Stenz, Gernot: The disconnection tableau calculus (2007)
  8. Benzmüller, Christoph; Sorge, Volker; Jamnik, Mateja; Kerber, Manfred: Can a higher-order and a first-order theorem prover cooperate? (2005)
  9. Otten, Jens; Bibel, Wolfgang: IeanCOP: lean connection-based theorem proving (2003)
  10. Riazanov, Alexandre; Voronkov, Andrei: Limited resource strategy in resolution theorem proving (2003)
  11. Fuchs, Marc: Controlled use of clausal lemmas in connection tableau calculi (2000)
  12. Stenz, Gernot; Wolf, Andreas: E-SETHEO: An automated(^3) theorem prover (2000)
  13. Bibel, W.: Let’s plan it deductively! (1998)
  14. Fischer, Bernd; Schumann, Johann; Snelting, Gregor: Deduction-based software component retrieval (1998)
  15. Fischer, Bernd; Schumann, Johann M. Ph.: SETHEO goes software engineering: application of ATP to software reuse (1997)
  16. Ibens, Ortrun; Letz, Reinhold: Subgoal alternation in model elimination (1997)
  17. Moser, Max; Ibens, Ortrun; Letz, Reinhold; Steinbach, Joachim; Goller, Christoph; Schumann, Johann; Mayr, Klaus: The CADE-13 systems SETHEO and E-SETHEO. (1997) ioport