{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T16:10:37Z","timestamp":1725466237855},"publisher-location":"Berlin, Heidelberg","reference-count":5,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540646754"},{"type":"electronic","value":"9783540691105"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0054255","type":"book-chapter","created":{"date-parts":[[2006,6,7]],"date-time":"2006-06-07T03:28:51Z","timestamp":1149650931000},"page":"134-138","source":"Crossref","is-referenced-by-count":3,"title":["System description: An interface between CLAM and HOL"],"prefix":"10.1007","author":[{"given":"Konrad","family":"Slind","sequence":"first","affiliation":[]},{"given":"Mike","family":"Gordon","sequence":"additional","affiliation":[]},{"given":"Richard","family":"Boulton","sequence":"additional","affiliation":[]},{"given":"Alan","family":"Bundy","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,5,25]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"R. J. Boulton. Combining decision procedures in the HOL system. In Proceedings of the 8th International Workshop on Higher Order Logic Theorem Proving and Its Applications, volume 971 of Lecture Notes in Computer Science. Springer, 1995.","DOI":"10.1007\/3-540-60275-5_58"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"R. Boulton, A. Bundy, K. Slind, and M. Gordon. A Prototype Interface between CLAM and HOL. Research Paper 854, Department of Artificial Intelligence, University of Edinburgh, June 1997.","DOI":"10.1007\/BFb0055131"},{"issue":"3","key":"16_CR3","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/BF00249016","volume":"7","author":"A. Bundy","year":"1991","unstructured":"A. Bundy, F. van Harmelen, J. Hesketh, and A. Smaill. Experiments with proof plans for induction. Journal of Automated Reasoning, 7(3):303\u2013324, 1991.","journal-title":"Journal of Automated Reasoning"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"A. P. Felty and D. J. Howe. Hybrid interactive theorem proving using Nuprl and HOL. In Proceedings of the 14th International Conference on Automated Deduction (CADE-I4), volume 1249 of Lecture Notes in Artificial Intelligence. Springer, 1997.","DOI":"10.1007\/3-540-63104-6_34"},{"key":"16_CR5","unstructured":"M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-15"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0054255","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,15]],"date-time":"2020-04-15T05:22:44Z","timestamp":1586928164000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0054255"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540646754","9783540691105"],"references-count":5,"URL":"https:\/\/doi.org\/10.1007\/bfb0054255","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}