{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T23:04:52Z","timestamp":1776553492866,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":6,"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_10","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T07:18:26Z","timestamp":1186903106000},"page":"134-138","source":"Crossref","is-referenced-by-count":16,"title":["An LCF-Style Interface between HOL and First-Order Logic"],"prefix":"10.1007","author":[{"given":"Joe","family":"Hurd","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,4]]},"reference":[{"key":"10_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1007\/10721959_10","volume-title":"Proceedings of the 17th International Conference on Automated Deduction (CADE-17)","author":"M. Bezem","year":"2000","unstructured":"Marc Bezem, Dimitri Hendriks, and Hans de Nivelle. Automated proof construction in type theory using resolution. In David A. McAllester, editor, Proceedings of the 17th International Conference on Automated Deduction (CADE-17), volume 1831 of Lecture Notes in Computer Science, pages 148\u2013163, Pittsburgh, PA, USA, June 2000. Springer."},{"key":"10_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF","author":"M. Gordon","year":"1979","unstructured":"M. Gordon, R. Milner, and C. Wadsworth. Edinburgh LCF, volume 78 of Lecture Notes in Computer Science, Springer Verlag, 1979."},{"key":"10_CR3","unstructured":"M. J. C. Gordon and T. F. Melham. Introduction to HOL (A theorem-proving environment for higher order logic). Cambridge University Press, 1993."},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"John Harrison. Optimizing proof search in model elimination. In Michael A. McRobbie and John K. Slaney, editors, 13th International Conference on Automated Deduction (CADE-13), volume 1104 of Lecture Notes in Artificial Intelligence, pages 313\u2013327, New Brunswick, NJ, USA, July 1996. Springer.","DOI":"10.1007\/3-540-61511-3_97"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"R. Kumar, T. Kropf, and K. Schneider. Integrating a first-order automatic prover in the HOL environment. In Myla Archer, Jeffrey J. Joyce, Karl N. Levitt, and Phillip J. Windley, editors, Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications (HOL\u2019 91), August 1991, pages 170\u2013176, Davis, CA, USA, 1992. IEEE Computer Society Press.","DOI":"10.1109\/HOL.1991.596284"},{"key":"10_CR6","unstructured":"L. C. Paulson. A generic tableau prover and its integration with Isabelle. Journal of Universal Computer Science, 5(3), March 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_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T08:51:34Z","timestamp":1737363094000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45620-1_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439318","9783540456209"],"references-count":6,"URL":"https:\/\/doi.org\/10.1007\/3-540-45620-1_10","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}