Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Holland, J.H.: Adaptation in Natural and Artificial Systems. MIT Press, Cambridge (1992)
Moser, M., et al.: SETHEO and E-SETHEO. The CADE-13 Systems. JAR 18(2), 237–246 (1997)
Schulz, S.: System Abstract: E 0.3. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 297–301. Springer, Heidelberg (1999)
Stenz, G., Wolf, A.: Strategy Selection by Genetic Programming. FLAIRS-12, 346–350 (1999)
Stenz, G., Wolf, A.: E-SETHEO: Design, Configuration and Use of a Parallel Automated Theorem Prover. In: Foo, N.Y. (ed.) AI 1999. LNCS (LNAI), vol. 1747, pp. 231–243. Springer, Heidelberg (1999)
Sutcliffe, G., et al.: The TPTP Prob. Lib. In: Bundy, A., et al. (eds.) CADE 1994. LNCS (LNAI), vol. 814, pp. 252–266. Springer, Heidelberg (1994)
Wolf, A., Letz, R.: Strategy Parallelism in ATP. IJPRAI 13(2), 219–245 (1999)
Wolf, A.: p-SETHEO: Strategy Parallelism in ATP. In: de Swart, H. (ed.) TABLEAUX 1998. LNCS (LNAI), vol. 1397, pp. 320–324. Springer, Heidelberg (1998)
Wolf, A.: Strategy Selection for Automated Theorem Proving. In: Giunchiglia, F. (ed.) AIMSA 1998. LNCS (LNAI), vol. 1480, pp. 452–465. Springer, Heidelberg (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Stenz, G., Wolf, A. (2000). E-SETHEO: An Automated3 Theorem Prover. In: Dyckhoff, R. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2000. Lecture Notes in Computer Science(), vol 1847. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10722086_34
Download citation
DOI: https://doi.org/10.1007/10722086_34
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67697-3
Online ISBN: 978-3-540-45008-5
eBook Packages: Springer Book Archive