{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,12]],"date-time":"2026-03-12T21:19:40Z","timestamp":1773350380834,"version":"3.50.1"},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2002,9,1]],"date-time":"2002-09-01T00:00:00Z","timestamp":1030838400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2002,9,1]],"date-time":"2002-09-01T00:00:00Z","timestamp":1030838400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[2002,9]]},"DOI":"10.1023\/a:1021935419355","type":"journal-article","created":{"date-parts":[[2003,3,21]],"date-time":"2003-03-21T23:56:29Z","timestamp":1048290989000},"page":"389-411","source":"Crossref","is-referenced-by-count":33,"title":["A Comparison of Mizar and Isar"],"prefix":"10.1007","volume":"29","author":[{"given":"Markus","family":"Wenzel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Freek","family":"Wiedijk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5109774_CR1","doi-asserted-by":"crossref","unstructured":"Aspinall, D.: Proof general: A generic tool for poof development, in European Joint Conferences on Theory and Practice of Software (ETAPS), 2000.","DOI":"10.1007\/3-540-46419-0_3"},{"key":"5109774_CR2","doi-asserted-by":"crossref","unstructured":"Bauer, G. and Wenzel, M.: Computer-assisted mathematics at work \u2013 The Hahn-Banach theorem in Isabelle\/Isar, in T. Coquand, P. Dybjer, B. Nordstr\u00f6m and J. Smith (eds), Types for Proofs and Programs: TYPES'99, LNCS 1956, 2000.","DOI":"10.1007\/3-540-44557-9_4"},{"key":"5109774_CR3","doi-asserted-by":"crossref","unstructured":"Bauer, G. and Wenzel, M.: Calculational reasoning revisited \u2013 An Isabelle\/Isar experience, in R. J. Boulton and P. B. Jackson (eds), Theorem Proving in Higher Order Logics: TPHOLs 2001, LNCS 2152, 2001.","DOI":"10.1007\/3-540-44755-5_7"},{"key":"5109774_CR4","doi-asserted-by":"crossref","unstructured":"Berghofer, S. and Nipkow, T.: Proof terms for simply typed higher order logic, in J. Harrison and M. Aagaard (eds), Theorem Proving in Higher Order Logics: TPHOLs 2000, LNCS 1869, 2000.","DOI":"10.1007\/3-540-44659-1_3"},{"key":"5109774_CR5","unstructured":"Burstall, R.: Teaching people to write proofs: A tool, in CafeOBJ Symposium, Numazu, Japan, 1998."},{"key":"5109774_CR6","volume-title":"Proceedings of theWorkshop on Programming Languages","author":"N. de Bruijn","year":"1987","unstructured":"de Bruijn, N.: The mathematical vernacular, a language for mathematics with typed sets, in P. Dybjer et al. (eds), Proceedings of theWorkshop on Programming Languages, Marstrand, Sweden, 1987."},{"key":"5109774_CR7","doi-asserted-by":"crossref","unstructured":"Harrison, J.: A Mizar mode for HOL, in Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics, TPHOLs'96, LNCS 1125, Springer, 1996.","DOI":"10.1007\/BFb0105406"},{"key":"5109774_CR8","volume-title":"An Outline of PC Mizar","author":"M. Muzalewski","year":"1993","unstructured":"Muzalewski, M.: An Outline of PC Mizar, Fondation Philippe le Hodey, Brussels, 1993. http:\/\/www.cs.kun.nl\/~freek\/mizar\/mizarmanual.ps.gz."},{"key":"5109774_CR9","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L. and Wenzel, M.: Isabelle\/HOL \u2013 A Proof Assistant for Higher-Order Logic, LNCS 2283, Springer, 2002.","DOI":"10.1007\/3-540-45949-9"},{"key":"5109774_CR10","doi-asserted-by":"crossref","unstructured":"Paulson, L. C.: The foundation of a generic theorem prover, J. Automated Reasoning\n5(3) (1989).","DOI":"10.1007\/BF00248324"},{"key":"5109774_CR11","doi-asserted-by":"crossref","unstructured":"Paulson, L.: Isabelle: A Generic Theorem Prover, LNCS 828, Springer, 1994.","DOI":"10.1007\/BFb0030541"},{"key":"5109774_CR12","unstructured":"Paulson, L.: The Isabelle reference manual, 2002a. http:\/\/isabelle.in.tum.de\/doc\/ref.pdf. A COMPARISON OF MIZAR AND ISAR 411"},{"key":"5109774_CR13","unstructured":"Paulson, L. C.: Isabelle's logics: FOL and ZF, 2002b. http:\/\/isabelle.in.tum.de\/doc\/logics-ZF.pdf."},{"key":"5109774_CR14","unstructured":"Rudnicki, P.: An overview of the MIZAR project, in 1992 Workshop on Types for Proofs and Programs, Bastad, 1992."},{"key":"5109774_CR15","unstructured":"Syme, D.: DECLARE: A prototype declarative proof system for higher order logic, Technical Report 416, University of Cambridge Computer Laboratory, 1997."},{"key":"5109774_CR16","unstructured":"Syme, D.: Declarative theorem proving for operational semantics, Ph.D. thesis, University of Cambridge, 1998."},{"key":"5109774_CR17","doi-asserted-by":"crossref","unstructured":"Syme, D.: Three tactic theorem proving, in Theorem Proving in Higher Order Logics, TPHOLs'99, Nice, France, LNCS 1690, Springer, 1999.","DOI":"10.1007\/3-540-48256-3_14"},{"key":"5109774_CR18","unstructured":"Trybulec, A.: Some features of the Mizar language, Presented at a workshop in Turin, Italy, 1993."},{"key":"5109774_CR19","doi-asserted-by":"crossref","unstructured":"Wenzel, M.: Isar \u2013 A generic interpretative approach to readable formal proof documents, in Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin and L. Thery (eds), Theorem Proving in Higher Order Logics: TPHOLs'99, LNCS 1690, 1999.","DOI":"10.1007\/3-540-48256-3_12"},{"key":"5109774_CR20","unstructured":"Wenzel, M.: Isabelle\/Isar \u2013 A versatile environment for human-readable formal proof documents, Ph.D. thesis, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, 2002a. http:\/\/tumb1.biblio.tu-muenchen.de\/publ\/diss\/in\/2002\/wenzel.html."},{"key":"5109774_CR21","unstructured":"Wenzel, M.: The Isabelle\/Isar Reference Manual, TU M\u00fcnchen, 2002b. http:\/\/isabelle.in.tum.de\/doc\/isar-ref.pdf."},{"key":"5109774_CR22","unstructured":"Wiedijk, F.: Mizar: An impression, 1993. http:\/\/www.cs.kun.nl\/~freek\/mizar\/mizarintro.ps.gz."},{"key":"5109774_CR23","unstructured":"Wiedijk, F.: The mathematical vernacular, 2000. http:\/\/www.cs.kun.nl\/~freek\/notes\/mv.ps.gz."},{"key":"5109774_CR24","doi-asserted-by":"crossref","unstructured":"Wiedijk, F.: Mizar light for HOL light, in R. J. Boulton and P. B. Jackson (eds), Theorem Proving in Higher Order Logics: TPHOLs 2001, LNCS 2152, 2001.","DOI":"10.1007\/3-540-44755-5_26"},{"key":"5109774_CR25","unstructured":"Wiedijk, F.: Formal proof sketches, 2002. http:\/\/www.cs.kun.nl\/~freek\/notes\/sketches.ps.gz."},{"key":"5109774_CR26","doi-asserted-by":"crossref","unstructured":"Zammit, V.: On the implementation of an extensible declarative proof language, in Theorem Proving in Higher Order Logics, TPHOLs'99, Nice, France, LNCS 1690, Springer, 1999a.","DOI":"10.1007\/3-540-48256-3_13"},{"key":"5109774_CR27","unstructured":"Zammit, V.: On the readability of machine checkable formal proofs, Ph.D. thesis, University of Kent, 1999b."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1021935419355.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1021935419355\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1021935419355.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:45:11Z","timestamp":1749123911000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1021935419355"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,9]]},"references-count":27,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2002,9]]}},"alternative-id":["5109774"],"URL":"https:\/\/doi.org\/10.1023\/a:1021935419355","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2002,9]]}}}