{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:59:39Z","timestamp":1725663579653},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540534143"},{"type":"electronic","value":"9783540468691"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1990]]},"DOI":"10.1007\/3-540-53414-8_49","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T17:02:29Z","timestamp":1330189349000},"page":"261-270","source":"Crossref","is-referenced-by-count":2,"title":["Representing heuristic-relevant information for an automated theorem prover"],"prefix":"10.1007","author":[{"given":"Christian B.","family":"Suttner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"23_CR1","unstructured":"[BES+81] K. Bl\u00e4sius, N. Eisinger, J. Siekmann, G. Smolka, A. Herold, and C. Walther. The Markgraf Karl Refutation Proof Procedure. In Proceedings of the Seventh International Joint Conference on Artificial Intelligence, Vancouver, 1981."},{"key":"23_CR2","unstructured":"C.-L. Chang and R.C.-T. Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1973."},{"key":"23_CR3","doi-asserted-by":"crossref","unstructured":"W. Ertel, J. Schumann, and C.B. Suttner. Learning Heuristics for a Theorem Prover using Back Propagation. In Proceedings of the 5. \u00d6GAI-Conference, Igls, Austria, 1989. Springer.","DOI":"10.1007\/978-3-642-74688-8_10"},{"key":"23_CR4","unstructured":"R. Letz, S. Bayerl, J. Schumann, and W. Bibel. SETHEO: A High-Performance Theorem Prover. to appear in: Journal of Automated Reasoning."},{"key":"23_CR5","doi-asserted-by":"crossref","unstructured":"D.W. Loveland. Mechanical Theorem-Proving by Model Elimination. Journal of the ACM, 15(2), 1968.","DOI":"10.1145\/321450.321456"},{"key":"23_CR6","doi-asserted-by":"crossref","unstructured":"R. Overbeek, J. McCharen, and L. Wos. Complexity and Related Enhancements for Automated Theorem-Proving Programs. Comp. & Maths. with Appls., 2(1-A), 1976.","DOI":"10.1016\/0898-1221(76)90002-X"},{"key":"23_CR7","doi-asserted-by":"crossref","unstructured":"D.E. Rumelhart, G.E. Hinton, and R.J. Williams. Learning Internal Representations by Error Propagation. In Parallel Distributed Processing, 1986.","DOI":"10.21236\/ADA164453"},{"key":"23_CR8","doi-asserted-by":"crossref","unstructured":"A.L. Samuel. Some Studies in Machine Learning Using the Game of Checkers. IBM Journal, 1(3), 1959.","DOI":"10.1147\/rd.33.0210"},{"key":"23_CR9","doi-asserted-by":"crossref","unstructured":"A.L. Samuel. Some Studies in Machine Learning Using the Game of Checkers, II. IBM Journal, 11(6), 1967.","DOI":"10.1147\/rd.116.0601"},{"key":"23_CR10","doi-asserted-by":"crossref","unstructured":"C.B. Suttner and W. Ertel. Automatic Acquisition of Search Guiding Heuristics. In Proceedings of the 10. International Conference on Automated Deduction (CADE). Springer, 1990.","DOI":"10.1007\/3-540-52885-7_108"},{"key":"23_CR11","doi-asserted-by":"crossref","unstructured":"J.R. Slagle and C.D. Farrell. Experiments in Automatic Learning for a Multipurpose Heuristic Program. Comm. of the ACM, 14(2), 1971.","DOI":"10.1145\/362515.362560"},{"key":"23_CR12","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1007\/BF00246025","volume":"2","author":"M.E. Stickel","year":"1986","unstructured":"M.E. Stickel. Schubert's Steamroller Problem: Formulations and Solutions. Journal of Automated Reasoning, 2:89\u2013101, 1986.","journal-title":"Journal of Automated Reasoning"},{"key":"23_CR13","unstructured":"C.B. Suttner. Learning Heuristics for Automated Theorem Proving. Diploma Thesis, Technical University Munich, May 1989."}],"container-title":["Lecture Notes in Computer Science","Aspects and Prospects of Theoretical Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-53414-8_49.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T15:49:57Z","timestamp":1605628197000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-53414-8_49"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990]]},"ISBN":["9783540534143","9783540468691"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-53414-8_49","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1990]]}}}