{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:30:32Z","timestamp":1774837832445,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540615873","type":"print"},{"value":"9783540706410","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/bfb0105406","type":"book-chapter","created":{"date-parts":[[2011,11,9]],"date-time":"2011-11-09T21:17:00Z","timestamp":1320873420000},"page":"203-220","source":"Crossref","is-referenced-by-count":32,"title":["A mizar mode for HOL"],"prefix":"10.1007","author":[{"given":"John","family":"Harrison","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2007,4,29]]},"reference":[{"key":"14_CR1","unstructured":"P. B. Andrews, M. Bishop, S. Issar, D. Nesmith, F. Pfenning, and H. Xi. TPS: A theorem proving system for classical type theory. Research report 94\u2013166, Department of Mathematics, Carnegie-Mellon University, 1994."},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"Anonymous. The QED Manifesto. In A. Bundy, editor, 12th International Conference on Automated Deduction, volume 814 of Lecture Notes in Computer Science, pages 238\u2013251, Nancy, France, 1994. Springer-Verlag.","DOI":"10.1007\/3-540-58156-1"},{"key":"14_CR3","volume-title":"Proceedings of the 1991 International Workshop on the HOL theorem proving system and its Applications","year":"1991","unstructured":"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, University of California at Davis, Davis CA, USA, 1991. IEEE Computer Society Press."},{"key":"14_CR4","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/BF00881804","volume":"15","author":"B. Beckert","year":"1995","unstructured":"B. Beckert and J. Posegga. leanT A P: Lean, tableau-based deduction. Journal of Automated Reasoning, 15:339\u2013358, 1995. Available on the Web from ftp:\/\/sonja.ira.uka.de\/pub\/posegga\/LeanTaP.ps.Z.","journal-title":"Journal of Automated Reasoning"},{"key":"14_CR5","doi-asserted-by":"crossref","first-page":"46","DOI":"10.1007\/3-540-60275-5_56","volume-title":"Higher Order Logic Theorem Proving and Its Applications: Proceedings of the 8th International Workshop","author":"P. E. Black","year":"1995","unstructured":"P. E. Black and P. J. Windley. Automatically synthesized term denotation predicates: A proof aid. In P. J. Windley, T. Schubert, and J. Alves-Foss, editors, Higher Order Logic Theorem Proving and Its Applications: Proceedings of the 8th International Workshop, volume 971 of Lecture Notes in Computer Science, pages 46\u201357, Aspen Grove, Utah, 1995. Springer-Verlag."},{"key":"14_CR6","series-title":"Technical Report","volume-title":"Efficiency in a fully-expansive theorem prover","author":"R. J. Boulton","year":"1993","unstructured":"R. J. Boulton. Efficiency in a fully-expansive theorem prover. Technical Report 337, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge, CB2 3QG, UK, 1993. Author's PhD thesis."},{"key":"14_CR7","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/BF02328452","volume":"2","author":"R. S. Boyer","year":"1986","unstructured":"R. S. Boyer, E. Lusk, W. McCune, R. Overbeek, M. Stickel, and L. Wos. Set theory in first order logic: Clauses for Goedel's axioms. Journal of Automated Reasoning, 2:287\u2013327, 1986.","journal-title":"Journal of Automated Reasoning"},{"key":"14_CR8","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1093\/comjnl\/38.2.91","volume":"38","author":"P. Curzon","year":"1995","unstructured":"P. Curzon. Tracking design changes with formal machine-checked proof. The Computer Journal, 38:91\u2013100, 1995.","journal-title":"The Computer Journal"},{"key":"14_CR9","first-page":"558","volume-title":"10th International Conference on Automated Deduction, volume 449 of Lecture Notes in Computer Science","author":"T. B. Tour de la","year":"1990","unstructured":"T. B. de la Tour. Minimizing the number of clauses by renaming. In Stickel [34], pages 558\u2013572."},{"key":"14_CR10","series-title":"Technical report","volume-title":"Simultaneous rigid E-unification is undecidable","author":"A. Degtyarev","year":"1995","unstructured":"A. Degtyarev and A. Voronkov. Simultaneous rigid E-unification is undecidable. Technical report 105, Computing Science Department, Uppsala University, Box 311, S-751 05 Uppsala, Sweden, 1995. Also available on the Web as ftp:\/\/ftp.csd.uu.se\/pub\/papers\/reports\/0105.ps.gz."},{"key":"14_CR11","unstructured":"G. Dowek. Collections, sets and types. Technical report 2708, INRIA Roquencourt, 1995."},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"A. J. M. van Gasteren. On the shape of mathematical arguments, volume 445 of Lecture Notes in Computer Science. Springer-Verlag, 1990. Foreword by E. W. Dijkstra.","DOI":"10.1007\/BFb0020908"},{"key":"14_CR13","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":"14_CR14","doi-asserted-by":"crossref","unstructured":"M. J. C. Gordon, R. 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"},{"key":"14_CR15","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1109\/HOL.1991.596285","volume-title":"Proceedings of the 1991 International Workshop on the HOL theorem proving system and its Applications","author":"J. Grundy","year":"1991","unstructured":"J. Grundy. Window inference in the HOL system. In Archer et al. [3]. pages 177\u2013189."},{"key":"14_CR16","unstructured":"J. Grundy. A browsable format for proof presentation. In C. Gefwert, P. Orponen, and J. Sepp\u00e4nen, editors, Proceedings of the Finnish Artificial Intelligence Society Symposium: Logic, Mathematics and the Computer, volume 14 of Suomen Teko\u00e4lyseuran julkaisuja, pages 171\u2013178. Finnish Artificial Intelligence Society, 1996."},{"key":"14_CR17","series-title":"Technical Report","volume-title":"Metatheory and reflection in theorem proving: A survey and critique","author":"J. Harrison","year":"1995","unstructured":"J. Harrison. Metatheory and reflection in theorem proving: A survey and critique. Technical Report CRC-053, SRI Cambridge, Millers Yard, Cambridge, UK, 1995. Available on the Web as http:\/\/www.cl.cam.ac.uk\/users\/jrh\/papers\/reflect.dvi.gz."},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"J. Harrison. Optimizing proof search in model elimination. To appear in the proceedings of the 13th International Conference on Automated Deduction (CADE 13), Springer Lecture Notes in Computer Science, 1996.","DOI":"10.1007\/3-540-61511-3_97"},{"key":"14_CR19","unstructured":"J. Harrison and K. Slind. A reference version of HOL. Presented in poster session of 1994 HOL Users Meeting and only published in participants\u2019 supplementary proceedings. Available on the Web from http:\/\/www.dcs.glasgow.ac.uk\/~hug94\/sproc.html, 1994."},{"key":"14_CR20","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G. Huet","year":"1975","unstructured":"G. Huet. A unification algorithm for typed \u03bb-calculus. Theoretical Computer Science, 1:27\u201357, 1975.","journal-title":"Theoretical Computer Science"},{"key":"14_CR21","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1109\/HOL.1991.596284","volume-title":"Proceedings of the 1991 International Workshop on the HOL theorem proving system and its Applications","author":"R. Kumar","year":"1991","unstructured":"R. Kumar, T. Kropf, and K. Schneider. Integrating a first-order automatic prover in the HOL environment. In Archer et al. [3], pages 170\u2013176."},{"key":"14_CR22","first-page":"246","volume-title":"Proceedings of the 8th National Conference on Artificial Intelligence","author":"W. McCune","year":"1990","unstructured":"W. McCune. Equality in automated deduction. In: T. Dietterich and W. Swartout, editors, Proceedings of the 8th National Conference on Artificial Intelligence, pages 246\u2013252, Boston, MA, 1990. MIT Press."},{"key":"14_CR23","doi-asserted-by":"crossref","unstructured":"T. F. Melham. Automating recursive type definitions in higher order logic. In G. Birtwistle and P. A. Subrahmanyam, editors, Current Trends in Hardware Verification and Automated Theorem Proving, pages 341\u2013386. Springer-Verlag, 1989.","DOI":"10.1007\/978-1-4612-3658-0_9"},{"key":"14_CR24","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1109\/HOL.1991.596299","volume-title":"Proceedings of the 1991 International Workshop on the HOL theorem proving system and its Applications","author":"T. F. Melham","year":"1991","unstructured":"T. F. Melham. A package for inductive relation definitions in HOL. In Archer et al. [3], pages 350\u2013357."},{"key":"14_CR25","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/0167-6423(83)90008-4","volume":"3","author":"L. C. Paulson","year":"1983","unstructured":"L. C. Paulson. A higher-order implementation of rewriting. Science of Computer Programming, 3:119\u2013149, 1983.","journal-title":"Science of Computer Programming"},{"key":"14_CR26","doi-asserted-by":"crossref","unstructured":"L. C. Paulson. Isabelle: a generic theorem prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994. With contributions by Tobias Nipkow.","DOI":"10.1007\/BFb0030541"},{"key":"14_CR27","first-page":"475","volume-title":"Proceedings of the 1993 International Workshop on the HOL theorem proving system and its applications, volume 780 of Lecture Notes in Computer Science","author":"I. S. W. B. Prasetya","year":"1993","unstructured":"I. S. W. B. Prasetya. On the style of mechanical proving. In J. J. Joyce and C. Seger, editors, Proceedings of the 1993 International Workshop on the HOL theorem proving system and its applications, volume 780 of Lecture Notes in Computer Science, pages 475\u2013488, UBC, Vancouver, Canada, 1993. Springer-Verlag."},{"key":"14_CR28","unstructured":"J. A. Robinson. A note on mechanizing higher order logic. In B. Meltzer and D. Michie, editors, Machine Intelligence 5, pages 123\u2013133. Edinburgh University Press, 1969."},{"key":"14_CR29","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1093\/logcom\/3.1.47","volume":"3","author":"P. J. Robinson","year":"1993","unstructured":"P. J. Robinson and J. Staples. Formalizing a hierarchical structure of practical mathematical reasoning. Journal of Logic and Computation, 3:47\u201361, 1993.","journal-title":"Journal of Logic and Computation"},{"key":"14_CR30","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/BF00247436","volume":"3","author":"P. Rudnicki","year":"1987","unstructured":"P. Rudnicki, Obvious inferences. Journal of Automated Reasoning, 3:383\u2013393, 1987.","journal-title":"Journal of Automated Reasoning"},{"key":"14_CR31","series-title":"Technical Report","volume-title":"Object language embedding in standard ml of new jersey","author":"K. Slind","year":"1991","unstructured":"K. Slind. Object language embedding in standard ml of new jersey. Technical Report 91-454-38, University of Calgary Computer Science Department, 2500 University Drive N. W., Calgary, Alberta, Canada, TN2 1N4, 1991. Also appeared in Proceedings of 2nd ML Workshop."},{"key":"14_CR32","unstructured":"S. Sokolowski. A note on tactics in LCF. Technical Report CSR-140-83, University of Edinburgh, Department of Computer Science, 1983."},{"key":"14_CR33","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/BF00297245","volume":"4","author":"M. E. Stickel","year":"1988","unstructured":"M. E. Stickel. A Prolog Technology Theorem Prover: Implementation by an extended Prolog compiler. Journal of Automated Reasoning, 4:353\u2013380, 1988.","journal-title":"Journal of Automated Reasoning"},{"key":"14_CR34","volume-title":"10th International Conference on Automated Deduction, volume 449 of Lecture Notes in Computer Science","year":"1990","unstructured":"M. E. Stickel, editor. 10th International Conference on Automated Deduction, volume 449 of Lecture Notes in Computer Science, Kaiserslautern, Federal Republic of Germany, 1990. Springer-Verlag."},{"key":"14_CR35","first-page":"322","volume-title":"10th International Conference on Automated Deduction, volume 449 of Lecture Notes in Computer Science","author":"M. Tarver","year":"1990","unstructured":"M. Tarver. An examination of the Prolog Technology Theorem-Prover. In Stickel [34]. Springer-Verlag pages 322\u2013335."},{"key":"14_CR36","first-page":"406","volume-title":"Logics of Programs, volume 193 of Lecture Notes in Computer Science","author":"A. Trybulec","year":"1985","unstructured":"A. Trybulec and H. A. Blair. Computer aided reasoning. In R. Parikh, editor, Logics of Programs, volume 193 of Lecture Notes in Computer Science, pages 406\u2013412, Brooklyn, 1985. Springer-Verlag."},{"key":"14_CR37","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1016\/0020-0190(87)90166-9","volume":"25","author":"J. G. Wiltink","year":"1987","unstructured":"J. G. Wiltink. A deficiency of natural deduction. Information Processing Letters, 25:233\u2013234, 1987.","journal-title":"Information Processing Letters"}],"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\/BFb0105406","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,19]],"date-time":"2019-06-19T09:44:21Z","timestamp":1560937461000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0105406"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540615873","9783540706410"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/bfb0105406","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996]]}}}