{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T21:24:30Z","timestamp":1742937870393,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540675570"},{"type":"electronic","value":"9783540454861"}],"license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-45486-1_21","type":"book-chapter","created":{"date-parts":[[2007,7,31]],"date-time":"2007-07-31T21:56:59Z","timestamp":1185919019000},"page":"254-266","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Scheduling Methods for Parallel Automated Theorem Proving"],"prefix":"10.1007","author":[{"given":"Gernot","family":"Stenz","sequence":"first","affiliation":[]},{"given":"Andreas","family":"Wolf","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2000,5,19]]},"reference":[{"key":"21_CR1","doi-asserted-by":"crossref","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"},{"key":"21_CR2","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.","DOI":"10.1007\/3-540-63104-6_7"},{"issue":"2","key":"21_CR3","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":"21_CR4","doi-asserted-by":"crossref","unstructured":"J. H. Holland. Adaptation in Natural and Artificial Systems. MIT Press, 1992.","DOI":"10.7551\/mitpress\/1090.001.0001"},{"key":"21_CR5","unstructured":"R. Letz. Clausal Tableaux. In Wolfgang Bibel and Peter H. Schmitt, editors, Automated Deduction \u2014 A Basis for Applications, volume I: Foundations, pages 43\u201372. Kluwer, Dordrecht, 1998."},{"issue":"2","key":"21_CR6","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1023\/A:1005808119103","volume":"18","author":"M.I.L.+.9.7._.M. Moser","year":"1997","unstructured":"[MIL+97]_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"},{"key":"21_CR7","doi-asserted-by":"crossref","unstructured":"S. Schulz. System Abstract: E 0.3. CADE-16, LNAI 1632, pp. 297\u201360. 1999.","DOI":"10.1007\/3-540-48660-7_27"},{"key":"21_CR8","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.","DOI":"10.1007\/3-540-52885-7_78"},{"key":"21_CR9","unstructured":"G. Stenz and A. Wolf. Strategy Selection by Genetic Programming. FLAIRS-12, pp. 346\u2013350. 1999."},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"G. Stenz and A. Wolf. E-SETHEO: Design, Configuration and Use of a Parallel Automated Theorem Prover. 12th Australian Joint Conference on Artificial Intelligence, LNAI 1747. 1999.","DOI":"10.1007\/3-540-46695-9_20"},{"key":"21_CR11","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.","DOI":"10.1007\/3-540-58156-1_35"},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"G. Sutcliffe, C. Suttner, and T. Yemenis. The TPTP Problem Library. CADE-12, LNAI 814, pp. 252\u2013266. 1994.","DOI":"10.1007\/3-540-58156-1_18"},{"key":"21_CR13","unstructured":"A. Voronkov. CASC 16 1\/2. Preprint CSPP-4, Department of Computer Science, University of Manchester, February 2000. \n                    http:\/\/www.cs.man.ac.uk\/preprints\/index.html"},{"key":"21_CR14","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.","DOI":"10.1007\/3-540-61511-3_75"},{"issue":"2","key":"21_CR15","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"},{"key":"21_CR16","doi-asserted-by":"crossref","unstructured":"A. Wolf. p-SETHEO: Strategy Parallelism in Automated Theorem Proving. TABLEAUX-98, LNAI 1397, pp. 320\u2013324. 1998.","DOI":"10.1007\/3-540-69778-0_32"},{"key":"21_CR17","doi-asserted-by":"crossref","unstructured":"A. Wolf. Strategy Selection for Automated Theorem Proving. AIMSA-98, LNAI 1480, pp. 452\u2013465. 1998.","DOI":"10.1007\/BFb0057466"}],"container-title":["Lecture Notes in Computer Science","Advances in Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45486-1_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T20:19:14Z","timestamp":1558469954000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45486-1_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540675570","9783540454861"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-45486-1_21","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]},"assertion":[{"value":"19 May 2000","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}