{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:30:47Z","timestamp":1774837847420,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540664635","type":"print"},{"value":"9783540482567","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48256-3_21","type":"book-chapter","created":{"date-parts":[[2007,8,3]],"date-time":"2007-08-03T16:15:22Z","timestamp":1186157722000},"page":"311-321","source":"Crossref","is-referenced-by-count":28,"title":["Integrating Gandalf and HOL"],"prefix":"10.1007","author":[{"given":"Joe","family":"Hurd","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,9,17]]},"reference":[{"key":"21_CR1","doi-asserted-by":"crossref","unstructured":"Wolfgang Ahrendt, Bernhard Beckert, Reiner H\u00e4hnle, Wolfram Menzel, Wolfgang Reif, Gerhard Schellhorn, and Peter H. Schmitt. Integration of automated and interactive theorem proving. In W. Bibel and P. Schmitt, editors, Automated Deduction: A Basis for Applications, volume II, chapter 4, pages 97\u2013116. Kluwer, 1998.","DOI":"10.1007\/978-94-017-0435-9_4"},{"key":"21_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58450-1_37","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"H. Busch","year":"1994","unstructured":"H. Busch. First-order automation for higher-order-logic theorem proving. In Higher Order Logic Theorem Proving and Its Applications, volume Lecture Notes in Computer Science volume 859. Springer-Verlag, 1994."},{"key":"21_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":"21_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"313","DOI":"10.1007\/3-540-61511-3_97","volume-title":"13th International Conference on Automated Deduction","author":"J. Harrison","year":"1996","unstructured":"J. Harrison. Optimizing proof search in model elimination. In M. A. McRobbie and J. K. Slaney, editors, 13th International Conference on Automated Deduction, volume 1104 of Lecture Notes in Computer Science, pages 313\u2013327, New Brunswick, NJ, 1996. Springer-Verlag."},{"key":"21_CR5","unstructured":"J. Harrison. The HOL-Light Manual (1.0), May 1998. Available from http:\/\/www.cl.cam.ac.uk\/users\/jrh\/hol-light\/ ."},{"key":"21_CR6","doi-asserted-by":"crossref","unstructured":"R. Kumar, Th. Kropf, and Schneider K. Integrating a first-order automatic prover in the hol environment. In M. Archer, J. J. Joyce, K. N. Levitt, and P. J. Windley, editors, Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications (HOL91), pages 170\u2013176, Davis, California, August 1991. IEEE Computer Society Press.","DOI":"10.1109\/HOL.1991.596284"},{"key":"21_CR7","unstructured":"K. Slind. HOL98 Draft User\u2019s Manual, Athabasca Release, Version 2, January 1999. Available from http:\/\/www.cl.cam.ac.uk\/users\/kxs\/ ."},{"key":"21_CR8","series-title":"Lect Notes Comput Sci","volume-title":"Cade 13","author":"T. Tammet","year":"1996","unstructured":"T. Tammet. A resolution theorem prover for intuitionistic logic. In Cade 13, volume Lecture Notes in Computer Science volume 1104. Springer Verlag, 1996."},{"key":"21_CR9","unstructured":"T. Tammet. Gandalf version c-1.0c Reference Manual, October 1997. Available from http:\/\/www.cs.chalmers.se\/~tammet\/ ."},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"T. Tammet. Towards efficient subsumption. In Automated Deduction: Cade 15, volume Lecture Notes in Artificial Intelligence volume 1421. Springer, 1998.","DOI":"10.1007\/BFb0054276"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48256-3_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T14:58:41Z","timestamp":1556722721000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48256-3_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664635","9783540482567"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/3-540-48256-3_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1999]]}}}