{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,14]],"date-time":"2026-02-14T09:02:39Z","timestamp":1771059759555,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540439318","type":"print"},{"value":"9783540456209","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45620-1_24","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T07:18:26Z","timestamp":1186903106000},"page":"285-289","source":"Crossref","is-referenced-by-count":16,"title":["The HR Program for Theorem Generation"],"prefix":"10.1007","author":[{"given":"Simon","family":"Colton","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,4]]},"reference":[{"key":"24_CR1","unstructured":"S. Colton. Automated Theory Formation in Pure Mathematics. PhD thesis, Department of Artificial Intelligence, University of Edinburgh, 2000."},{"key":"24_CR2","unstructured":"S. Colton, A. Bundy, and T. Walsh. Automatic identification of mathematical concepts. In Machine Learning: Proceedings of the 17th International Conference, 2000."},{"issue":"3","key":"24_CR3","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1006\/ijhc.2000.0394","volume":"53","author":"S. Colton","year":"2000","unstructured":"S. Colton, A. Bundy, and T. Walsh. On the notion of interestingness in automated mathematical discovery. IJHCS, 53(3):351\u2013375, 2000.","journal-title":"IJHCS"},{"key":"24_CR4","doi-asserted-by":"crossref","unstructured":"S. Colton and I Miguel. Constraint generation via automated theory formation. In Proceedings of CP-01, 2001.","DOI":"10.1007\/3-540-45578-7_42"},{"key":"24_CR5","unstructured":"S. Colton and G. Sutcliffe. Automatic Generation of Benchmark Problems for ATP Systems. In Proceedings of the 7th Symposium on AI and Mathematics, 2002."},{"key":"24_CR6","doi-asserted-by":"crossref","unstructured":"Andreas Franke and Michael Kohlhase. Mathweb, an agent-based communication layer for distributed automated theorem proving. In CADE 16, 1999.","DOI":"10.1007\/3-540-48660-7_17"},{"key":"24_CR7","doi-asserted-by":"crossref","unstructured":"P. Jackson. Computing prime implicates incrementally. In CADE 11, 1992.","DOI":"10.1007\/3-540-55602-8_170"},{"key":"24_CR8","unstructured":"W. McCune. The OTTER user\u2019s guide. Technical Report ANL\/90\/9, Argonne National Laboratories, 1990."},{"key":"24_CR9","unstructured":"W. McCune. A Davis-Putnam program and its application to finite first-order model search. Technical Report ANL\/MCS-TM-194, Argonne National Laboratories, 1994."},{"issue":"2","key":"24_CR10","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1023\/A:1005806324129","volume":"21","author":"G. Sutcliffe","year":"1998","unstructured":"G. Sutcliffe and C. Suttner. The TPTP Problem Library: CNF Release v1.2.1. Journal of Automated Reasoning, 21(2):177\u2013203, 1998. http:\/\/www.cs.miami.edu\/~tptp\/ .","journal-title":"Journal of Automated Reasoning"},{"key":"24_CR11","unstructured":"J. Zhang. MCS: Model-based conjecture searching. In CADE-16, 1999."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-18"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45620-1_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T23:56:17Z","timestamp":1556754977000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45620-1_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439318","9783540456209"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-45620-1_24","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}