{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:06:08Z","timestamp":1749125168059,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540668220"},{"type":"electronic","value":"9783540466956"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-46695-9_20","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T08:37:07Z","timestamp":1186907827000},"page":"231-243","source":"Crossref","is-referenced-by-count":5,"title":["E-SETHEO: Design, Configuration and Use of a Parallel Automated Theorem Prover"],"prefix":"10.1007","author":[{"given":"Gernot","family":"Stenz","sequence":"first","affiliation":[]},{"given":"Andreas","family":"Wolf","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"20_CR1","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1613\/jair.518","volume":"9","author":"D. J. Cook","year":"1998","unstructured":"D. J. Cook and R. C. Varnell. Adaptive Parallel Iterative Deepening Search. JAIR, 9:139\u2013165, 1998.","journal-title":"JAIR"},{"unstructured":"J. Denzinger. Knowledge-Based Distributed Search Using Teamwork. ICMAS-95, pp. 81\u201388. 1995.","key":"20_CR2"},{"unstructured":"J. Denzinger and M. Fuchs. Experiments in Learning Prototypical Situations for Variants of the Pursuit Game. ICMAS-96, pp. 48\u201355. 1996.","key":"20_CR3"},{"doi-asserted-by":"crossref","unstructured":"B. I. Dahn, J. Gehne, T. Honigmann, and A. Wolf. Integration of Automated and Interactive Theorem Proving in ILF. CADE-14, LNAI 1249, pp. 57\u201360. 1997.","key":"20_CR4","DOI":"10.1007\/3-540-63104-6_7"},{"issue":"2","key":"20_CR5","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1023\/A:1005879229581","volume":"18","author":"J. Denzinger","year":"1997","unstructured":"J. Denzinger, M. Kronenburg, and S. Schulz. DISCOUNT. A Distributed and Learning Equational Prover. JAR, 18(2):189\u2013198, 1997.","journal-title":"JAR"},{"key":"20_CR6","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-94-017-0437-3_11","volume":"III","author":"B. Fischer","year":"1998","unstructured":"B. Fischer, J. Schumann, and G. Snelting. Deduction Based Software Retrieval. Automated Deduction. A Basis for Applications. Volume III, pp. 265\u2013292. Kluwer, 1998.","journal-title":"Automated Deduction. A Basis for Applications"},{"doi-asserted-by":"crossref","unstructured":"J. H. Holland. Adaptation in Natural and Artificial Systems. MIT Press, 1992.","key":"20_CR7","DOI":"10.7551\/mitpress\/1090.001.0001"},{"unstructured":"R. E. Korf. Depth-First Iterative-Deepening: An Optimal Admissible Tree Search. Expert Systems, A Software Methodology for Modern Applications, pp. 380\u2013389. IEEE Computer Society Press, 1990.","key":"20_CR8"},{"unstructured":"J. R. Koza. Genetic Programming. MIT Press, 1992.","key":"20_CR9"},{"issue":"3","key":"20_CR10","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/BF00881947","volume":"13","author":"R. Letz","year":"1994","unstructured":"R. Letz, K. Mayr, and C. Goller. Controlled Integration of the Cut Rule into Connection Tableau Calculi. JAR, 13(3):297\u2013338, 1994.","journal-title":"JAR"},{"unstructured":"D. W. Loveland. Automated Theorem Proving: a Logical Basis. North-Holland, 1978.","key":"20_CR11"},{"issue":"2","key":"20_CR12","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1023\/A:1005808119103","volume":"18","author":"M. Moser","year":"1997","unstructured":"M. Moser, O. Ibens, R. Letz, J. Steinbach, C. Goller, J. Schumann, and K. Mayr. SETHEO and E-SETHEO. The CADE-13 Systems. JAR, 18(2):237\u2013246, 1997.","journal-title":"JAR"},{"doi-asserted-by":"crossref","unstructured":"J. Schumann. Using SETHEO for Verifying the Development of a Communication Protocol in Focus \u2014 A Case Study. TABLEAUX-95, LNAI 918, pp. 338\u2013352. 1995.","key":"20_CR13","DOI":"10.1007\/3-540-59338-1_46"},{"doi-asserted-by":"crossref","unstructured":"S. Schulz. System Abstract: E 0.3. CADE-16, LNAI 1632, pp. 297\u201360. 1999.","key":"20_CR14","DOI":"10.1007\/3-540-48660-7_27"},{"doi-asserted-by":"crossref","unstructured":"J. Schumann and R. Letz. PARTHEO: A High-Performance Parallel Theorem Prover. CADE-10, LNAI 449, pp. 40\u201356. 1990.","key":"20_CR15","DOI":"10.1007\/3-540-52885-7_78"},{"unstructured":"G. Stenz and A. Wolf. Strategy Selection by Genetic Programming. FLAIRS-12, pp. 346\u2013350. 1999.","key":"20_CR16"},{"doi-asserted-by":"crossref","unstructured":"D. B. Sturgill and A. M. Segre. A Novel Asynchronous Parallelism Scheme for First-Order Logic. CADE-12, LNAI 814, pp. 484\u2013498. 1994.","key":"20_CR17","DOI":"10.1007\/3-540-58156-1_35"},{"doi-asserted-by":"crossref","unstructured":"C. Suttner and J. Schumann. Parallel Automated Theorem Proving. PPAI-94, pp. 209\u2013257. 1994.","key":"20_CR18","DOI":"10.1016\/B978-0-444-81704-4.50015-6"},{"unstructured":"G. Sutcliffe and D. Seyfang. Smart Selective Competition Parallelism ATP. FLAIRS-99, pp. 341\u2013345. 1999.","key":"20_CR19"},{"doi-asserted-by":"crossref","unstructured":"G. Sutcliffe, C. Suttner, and T. Yemenis. The TPTP Problem Library. CADE-12, LNAI 814, pp. 252\u2013266. 1994.","key":"20_CR20","DOI":"10.1007\/3-540-58156-1_18"},{"doi-asserted-by":"crossref","unstructured":"C. Weidenbach, B. Gaede and G. Rock. SPASS & FLOTTER version 0.42. CADE-13, LNAI 1104, pp. 141\u2013145. 1996.","key":"20_CR21","DOI":"10.1007\/3-540-61511-3_75"},{"issue":"2","key":"20_CR22","first-page":"219","volume":"13","author":"A. Wolf","year":"1999","unstructured":"A. Wolf and R. Letz. Strategy Parallelism in Automated Theorem Proving. IJPRAI, 13(2):219\u2013245, 1999.","journal-title":"IJPRAI"},{"doi-asserted-by":"crossref","unstructured":"A. Wolf. p-SETHEO: Strategy Parallelism in Automated Theorem Proving. TABLEAUX-98, LNAI 1397, pp. 320\u2013324. 1998.","key":"20_CR23","DOI":"10.1007\/3-540-69778-0_32"},{"doi-asserted-by":"crossref","unstructured":"A. Wolf. Strategy Selection for Automated Theorem Proving. AIMSA-98, LNAI 1480, pp. 452\u2013465. 1998.","key":"20_CR24","DOI":"10.1007\/BFb0057466"}],"container-title":["Lecture Notes in Computer Science","Advanced Topics in Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46695-9_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,29]],"date-time":"2024-11-29T01:06:39Z","timestamp":1732842399000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/3-540-46695-9_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540668220","9783540466956"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-46695-9_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]}}}