{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:06:04Z","timestamp":1749125164091},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540649878"},{"type":"electronic","value":"9783540498018"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0055131","type":"book-chapter","created":{"date-parts":[[2006,7,27]],"date-time":"2006-07-27T09:09:13Z","timestamp":1153991353000},"page":"87-104","source":"Crossref","is-referenced-by-count":19,"title":["An interface between CLAM and HOL"],"prefix":"10.1007","author":[{"given":"Richard","family":"Boulton","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Konrad","family":"Slind","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alan","family":"Bundy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mike","family":"Gordon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,5,27]]},"reference":[{"key":"6_CR1","first-page":"252","volume-title":"volume 1249 of Lecture Notes in Artificial Intelligence","author":"C. Benzm\u00fcller","year":"1997","unstructured":"C. Benzm\u00fcller, L. Cheikhrouhou, D. Fehrer, A. Fiedler, X. Huang, M. Kerber, M. Kohlhase, K. Konrad, E. Melis, A. Meier, W. Schaarschmidt, J. Siekmann, and V. Sorge. \u03a9Mega: Towards a mathematical assistant. In McCune [12]., pages 252\u2013255."},{"key":"6_CR2","volume-title":"volume 971 of Lecture Notes in Computer Science","author":"R. J. Boulton","year":"1995","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, Aspen Grove, Utah, USA, September 1995. Springer-Verlag."},{"key":"6_CR3","volume-title":"Technical Report 390","author":"R. J. Boulton","year":"1996","unstructured":"R. J. Boulton. Syn: A single language for specifying abstract syntax trees, lexical analysis, parsing and pretty-printing. Technical Report 390, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge CB2 3QG, UK, March 1996."},{"key":"6_CR4","volume-title":"A Computational Logic Handbook, volume 23 of Perspectives in Computing","author":"R. S. Boyer","year":"1988","unstructured":"R. S. Boyer and J. S. Moore. A Computational Logic Handbook, volume 23 of Perspectives in Computing. Academic Press, San Diego, 1988."},{"key":"6_CR5","first-page":"647","volume-title":"volume 449 of Lecture Notes in Artificial Intelligence","author":"A. Bundy","year":"1990","unstructured":"A. Bundy, F. van Harmelen, C. Horn, and A. Smaill. The OYSTER-CLAM system. In M. E. Stickel, editor, Proceedings of the 10th International Conference on Automated Deduction, volume 449 of Lecture Notes in Artificial Intelligence, pages 647\u2013648, Kaiserslautern, FRG, July 1990. Springer-Verlag."},{"key":"6_CR6","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1016\/0004-3702(93)90079-Q","volume":"62","author":"A. Bundy","year":"1993","unstructured":"A. Bundy, A. Stevens, F. van Harmelen, A. Ireland, and A. Smaill. Rippling: A heuristic for guiding inductive proofs. Artificial Intelligence, 62:185\u2013253, 1993.","journal-title":"Artificial Intelligence"},{"issue":"3","key":"6_CR7","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, September 1991.","journal-title":"Journal of Automated Reasoning"},{"key":"6_CR8","first-page":"351","volume-title":"Lecture Notes in Artificial Intelligence","author":"A. P. Felty","year":"1997","unstructured":"A. P. Felty and D. J. Howe. Hybrid interactive theorem proving using Nuprl and HOL. In McCune [12], pages 351\u2013365."},{"key":"6_CR9","first-page":"157","volume-title":"volume 3 of Applied Logic Series","author":"F. Giunchiglia","year":"1996","unstructured":"F. Giunchiglia, P. Pecchiari, and C. Talcott. Reasoning theories \u2014 towards an architecture for open mechanized reasoning systems. In F. Baader and K. U. Schulz, editors, Proceedings of the First International Workshop on Frontiers of Combining Systems (FroCoS'96), volume 3 of Applied Logic Series, pages 157\u2013174, Munich, Germany, March 1996. Kluwer Academic Publishers."},{"key":"6_CR10","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."},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"M. J. Gordon, A. J. Milner, and C. P. Wadsworth. Edinburgh LCF: A Mechanised Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979.","DOI":"10.1007\/3-540-09724-4"},{"volume-title":"Lecture Notes in Artificial Intelligence","year":"1997","key":"6_CR12","unstructured":"W. McCune, editor. Proceedings of the 14th International Conference on Automated Deduction (CADE-14), volume 1249 of Lecture Notes in Artificial Intelligence, Townsville, North Queensland, Australia, July 1997. Springer."},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"L. C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994.","DOI":"10.1007\/BFb0030541"},{"key":"6_CR14","volume-title":"volume 1125 of Lecture Notes in Computer Science","author":"K. Slind","year":"1996","unstructured":"K. Slind. Function Definition in Higher Order Logic. In Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'96), volume 1125 of Lecture Notes in Computer Science, Turku, Finland, August 1996. Springer-Verlag."},{"key":"6_CR15","volume-title":"volume 1275 of Lecture Notes in Computer Science","author":"K. Slind","year":"1997","unstructured":"K. Slind. Derivation and Use of Induction Schemes in Higher-Order Logic. In Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'97), volume 1275 of Lecture Notes in Computer Science, Murray Hill, New Jersey, USA, August 1997. Springer-Verlag."},{"key":"6_CR16","first-page":"257","volume-title":"volume 1166 of Lecture Notes in Computer Science","author":"N. Shankar","year":"1996","unstructured":"N. Shankar PVS: Combining Specification, Proof Checking, and Model Checking. In Proceedings of the International Conference on Formal Methods in Computer-Aided Design (FMCAD'96), volume 1166 of Lecture Notes in Computer Science, Palo Alto, CA, USA, November 1996, pages 257\u2013264. Springer-Verlag."}],"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\/BFb0055131","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,11]],"date-time":"2019-02-11T18:16:20Z","timestamp":1549908980000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0055131"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540649878","9783540498018"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/bfb0055131","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}