{"id":23,"date":"2019-09-02T04:09:45","date_gmt":"2019-09-02T04:09:45","guid":{"rendered":"http:\/\/mizar-jp.org\/?page_id=23"},"modified":"2022-12-29T09:02:06","modified_gmt":"2022-12-29T00:02:06","slug":"%e3%83%81%e3%83%a5%e3%83%bc%e3%83%88%e3%83%aa%e3%82%a2%e3%83%ab","status":"publish","type":"page","link":"https:\/\/mizar-jp.org\/?page_id=23","title":{"rendered":"\u30c1\u30e5\u30fc\u30c8\u30ea\u30a2\u30eb"},"content":{"rendered":"\n<figure class=\"wp-block-image\"><img loading=\"lazy\" decoding=\"async\" width=\"1024\" height=\"192\" src=\"http:\/\/mizar-jp.org\/wp-content\/uploads\/2019\/09\/freelancer-763730_1280s-1024x192.jpg\" alt=\"\" class=\"wp-image-91\" srcset=\"https:\/\/mizar-jp.org\/wp-content\/uploads\/2019\/09\/freelancer-763730_1280s-1024x192.jpg 1024w, https:\/\/mizar-jp.org\/wp-content\/uploads\/2019\/09\/freelancer-763730_1280s-300x56.jpg 300w, https:\/\/mizar-jp.org\/wp-content\/uploads\/2019\/09\/freelancer-763730_1280s-768x144.jpg 768w, https:\/\/mizar-jp.org\/wp-content\/uploads\/2019\/09\/freelancer-763730_1280s.jpg 1280w\" sizes=\"auto, (max-width: 1024px) 100vw, 1024px\" \/><\/figure>\n\n\n\n<h3 class=\"wp-block-heading\">Hands-on tutorials<\/h3>\n\n\n\n<ul class=\"wp-block-list\">\n<li><a href=\"http:\/\/mizar.org\/cicm_tutorial\/mizar.pdf\">Introductory slides<\/a>\u00a0and\u00a0<a href=\"http:\/\/mizar.org\/cicm_tutorial\/\">Exercises<\/a>\u00a0for CICM Mizar hands-on tutorial<\/li>\n\n\n\n<li><a href=\"https:\/\/drive.google.com\/open?id=1SDIL0BhiwVHiceb6C9DwGuG4A11cCLaB\">Piotr Rudnicki, A Mizar demo\uff08\u30df\u30cb \u30c1\u30e5\u30fc\u30c8\u30ea\u30a2\u30eb\uff09\u65e5\u672c\u8a9e\u7248<\/a>&nbsp;\/&nbsp;<a href=\"https:\/\/drive.google.com\/open?id=1VS4F36R-BEovR3yhFwCR-3pInclKjRv9\">\u30aa\u30ea\u30b8\u30ca\u30eb<\/a><\/li>\n\n\n\n<li><a href=\"https:\/\/drive.google.com\/open?id=1hWAOCaIToqbIltqRFWEEZEdY8RsEgKyK\">Ewa Bonarska, An Introduction to PC Mizar \u65e5\u672c\u8a9e\u7248<\/a>&nbsp;\/&nbsp;<a href=\"https:\/\/drive.google.com\/open?id=1NFPZHc6bBc3QjzufX4vGFLJwVJS-G82W\">\u30aa\u30ea\u30b8\u30ca\u30eb<\/a><\/li>\n\n\n\n<li><a href=\"http:\/\/wiki.mizar.org\/\">Mizar TWiki<\/a><\/li>\n\n\n\n<li><a href=\"http:\/\/markun.cs.shinshu-u.ac.jp\/kiso\/projects\/proofchecker\/mizar\/index-j.html\">Mizar : \u30c1\u30e5\u30fc\u30c8\u30ea\u30a2\u30eb, \u30e9\u30a4\u30d6\u30e9\u30ea\u691c\u7d22, \u5404\u7a2e\u30ea\u30bd\u30fc\u30b9\uff08markun.cs\uff09<\/a><\/li>\n\n\n\n<li><a href=\"http:\/\/markun.cs.shinshu-u.ac.jp\/kiso\/projects\/proofchecker\/mizar\/Mizar4\/printout\/mizar4ja_prn.pdf\">Mizar\u8b1b\u7fa9\u9332 (\u6539\u8a02\u7b2c\u56db\u7248, PDF) \uff08markun.cs\uff09<\/a>\u203b\u30c4\u30fc\u30eb\u7fa4\u306e\u4f7f\u7528\u65b9\u6cd5\u306f53\u30da\u30fc\u30b8\u304b\u3089\u8a18\u8f09\u304c\u3042\u308a\u307e\u3059<\/li>\n<\/ul>\n\n\n\n<h3 class=\"wp-block-heading\">Mizar\u30b7\u30b9\u30c6\u30e0\u30fb\u30de\u30cb\u30e5\u30a2\u30eb<\/h3>\n\n\n\n<h4 class=\"wp-block-heading\">\u30d7\u30eb\u30fc\u30d5\u30c1\u30a7\u30c3\u30ab\uff0c\u30e9\u30a4\u30d6\u30e9\u30ea\u30c0\u30a6\u30f3\u30ed\u30fc\u30c9<\/h4>\n\n\n\n<ul class=\"wp-block-list\">\n<li><a href=\"http:\/\/mizar.org\/system\/index.html#download\">Current Mizar System Download (<\/a><a href=\"ftp:\/\/mizar.uwb.edu.pl\/pub\/system\/\">anonymous FTP from UWB) <\/a><a href=\"ftp:\/\/ftp.mizar.org\/\">(from ftp.mizar.org)<\/a><\/li>\n\n\n\n<li><a href=\"http:\/\/mizar.uwb.edu.pl\/~softadm\/pub\/system\/\">Current Mizar System Download (HTTP from UWB)<\/a> <a href=\"http:\/\/mirror.mizar-jp.org\/system\/index.html#download\">(from JAPAN mirror)<\/a><\/li>\n\n\n\n<li>Unpacked distribution can be browsed&nbsp;<a href=\"http:\/\/mizar.org\/version\/current\">here<\/a>&nbsp;(<a href=\"http:\/\/mizar.org\/version\/current\/html\/\">HTML-linked articles<\/a>,&nbsp;<a href=\"http:\/\/mizar.org\/version\/current\/mml\/\">plain-text articles<\/a>,&nbsp;<a href=\"http:\/\/mizar.org\/version\/current\/abstr\/\">abstracts<\/a>) <a href=\"http:\/\/mirror.mizar-jp.org\/version\/current\/\">(JAPAN mirror)<\/a><\/li>\n<\/ul>\n\n\n\n<h4 class=\"wp-block-heading\">Mizar\u30b7\u30b9\u30c6\u30e0\u306b\u95a2\u3059\u308b\u5404\u7a2e\u30ea\u30bd\u30fc\u30b9<\/h4>\n\n\n\n<ul class=\"wp-block-list\">\n<li><a href=\"http:\/\/mizar.org\/project\/\">Mizar Project<\/a><\/li>\n\n\n\n<li><a href=\"http:\/\/mizar.org\/language\/\">Mizar Language<\/a><\/li>\n\n\n\n<li><a href=\"http:\/\/mizar.org\/system\/\">Mizar System<\/a><\/li>\n\n\n\n<li><a href=\"http:\/\/mizar.org\/project\/bibliography.html\">Bibliography of Mizar Project<\/a><\/li>\n\n\n\n<li><a href=\"http:\/\/mizar.org\/people\/\">Mizar People<\/a><\/li>\n\n\n\n<li><a href=\"http:\/\/mizar.org\/library\/\">Mizar Mathematical Library<\/a><\/li>\n\n\n\n<li><a href=\"http:\/\/mizar.org\/fm\/\">Formalized Mathematics<\/a><\/li>\n\n\n\n<li><a href=\"http:\/\/mizar.org\/sum\/\">Association of Mizar Users<\/a><\/li>\n<\/ul>\n\n\n\n<h3 class=\"wp-block-heading\">Mizar\u30a2\u30fc\u30c6\u30a3\u30af\u30eb \u8a18\u8ff0\u652f\u63f4\u306b\u95a2\u3059\u308b\u5404\u7a2e\u30ea\u30bd\u30fc\u30b9<\/h3>\n\n\n\n<h4 class=\"wp-block-heading\">\u30a8\u30c7\u30a3\u30bf\u63f4\u7528\u30fb\u62e1\u5f35\u6a5f\u80fd<\/h4>\n\n\n\n<ul class=\"wp-block-list\">\n<li><a href=\"http:\/\/jurban.github.io\/mizarmode\/doc\/html\/MizarMode.html\">Mizar mode for Emacs<\/a><\/li>\n\n\n\n<li><a href=\"https:\/\/marketplace.visualstudio.com\/items?itemName=fpsbpkm.mizar-extension\">Mizar extension for VSCode<\/a><\/li>\n<\/ul>\n\n\n\n<h4 class=\"wp-block-heading\">\u30e9\u30a4\u30d6\u30e9\u30ea\u691c\u7d22<\/h4>\n\n\n\n<ul class=\"wp-block-list\">\n<li><a href=\"http:\/\/markun.cs.shinshu-u.ac.jp\/kiso\/projects\/proofchecker\/mizar\/index-j.html\">Mizar\u306e\u8cc7\u6e90\u3084\u30ea\u30f3\u30af\u3092\u5168\u3066\u96c6\u3081\u305f\u30b5\u30a4\u30c8\uff08Markun\uff09<\/a><\/li>\n\n\n\n<li><a href=\"http:\/\/mizar.uwb.edu.pl\/version\/current\/html\/\">HTML\u7248\u30e9\u30a4\u30d6\u30e9\u30ea\u95b2\u89a7<\/a><\/li>\n\n\n\n<li><a href=\"http:\/\/mmlquery.mizar.org\/mmlquery\/three.html\">MMLQuery\u691c\u7d22\u30c4\u30fc\u30eb Bancerek\u5148\u751f\u5236\u4f5c<\/a><\/li>\n\n\n\n<li><a rel=\"noreferrer noopener\" href=\"https:\/\/mimosa-project.github.io\/mmlreference\/current\/\" target=\"_blank\">MML\u7dcf\u5408\u691c\u7d22\u30c4\u30fc\u30eb \u4e2d\u6b63\u5148\u751f\u5236\u4f5c<\/a><\/li>\n\n\n\n<li><a href=\"https:\/\/em1.cs.shinshu-u.ac.jp\/emwiki\/release\/\">MML\u306e\u691c\u7d22\u30fb\u95b2\u89a7\u30fb\u6ce8\u8a18\u3092\u884c\u3046Web\u30b5\u30a4\u30c8(emwiki)\u3000\u4e2d\u6b63\u5148\u751f\u5236\u4f5c<\/a><\/li>\n\n\n\n<li><a href=\"http:\/\/grid01.ciirc.cvut.cz\/~mptp\/MizAR.html\">MizAR: parallelized AI\/ATP, verification, and presentation service for Mizar<\/a><\/li>\n<\/ul>\n\n\n\n<h4 class=\"wp-block-heading\">Mizar\u30d7\u30ed\u30b8\u30a7\u30af\u30c8<\/h4>\n\n\n\n<ul class=\"wp-block-list\">\n<li><a href=\"http:\/\/mizar.org\/system\/\">Mizar\u30d7\u30ed\u30b8\u30a7\u30af\u30c8\u672c\u90e8<\/a><\/li>\n\n\n\n<li><a href=\"https:\/\/www.degruyter.com\/view\/j\/forma\">\u5b66\u4f1a\u8a8c<\/a><\/li>\n\n\n\n<li><a href=\"http:\/\/mmlquery.mizar.org\/mmlquery\/fillin.php?filledfilename=mml-facts.mqt&amp;argument=number+102\">\u8457\u8005\u691c\u7d22<\/a><\/li>\n<\/ul>\n\n\n\n<h4 class=\"wp-block-heading\">\u4e8c\u6b21\u30c7\u30fc\u30bf\u30d9\u30fc\u30b9<\/h4>\n\n\n\n<ul class=\"wp-block-list\">\n<li><a href=\"http:\/\/zbmath.org\/authors\/\">bMath<\/a><\/li>\n\n\n\n<li><a href=\"http:\/\/www.scopus.com\/search\/form\/authorFreeLookup.url\">SCOPUS<\/a><\/li>\n\n\n\n<li><a href=\"http:\/\/mjl.clarivate.com\/cgi-bin\/jrnlst\/jlresults.cgi?PC=EX&amp;Full=formalized%20mathematics\">Web of Science Emerging Sources Citation Index<\/a><\/li>\n\n\n\n<li><a href=\"https:\/\/publons.com\/journal\/19354\/formalized-mathematics\">Publons \/ WoS Core Collection<\/a><\/li>\n\n\n\n<li><a href=\"https:\/\/dblp.uni-trier.de\/db\/journals\/fm\/\">DBLP<\/a><\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>Hands-on tutorials Mizar\u30b7\u30b9\u30c6\u30e0\u30fb\u30de\u30cb\u30e5\u30a2\u30eb \u30d7\u30eb\u30fc\u30d5\u30c1\u30a7\u30c3\u30ab\uff0c\u30e9\u30a4\u30d6\u30e9\u30ea\u30c0\u30a6\u30f3\u30ed\u30fc\u30c9 Mizar\u30b7\u30b9\u30c6\u30e0\u306b\u95a2\u3059\u308b\u5404\u7a2e\u30ea\u30bd\u30fc\u30b9 Mizar\u30a2\u30fc\u30c6\u30a3\u30af\u30eb \u8a18\u8ff0\u652f\u63f4\u306b\u95a2\u3059\u308b\u5404\u7a2e\u30ea\u30bd\u30fc\u30b9 \u30a8\u30c7\u30a3\u30bf\u63f4\u7528\u30fb [&hellip;]<\/p>\n","protected":false},"author":1,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-23","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/mizar-jp.org\/index.php?rest_route=\/wp\/v2\/pages\/23","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/mizar-jp.org\/index.php?rest_route=\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/mizar-jp.org\/index.php?rest_route=\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/mizar-jp.org\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/mizar-jp.org\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=23"}],"version-history":[{"count":21,"href":"https:\/\/mizar-jp.org\/index.php?rest_route=\/wp\/v2\/pages\/23\/revisions"}],"predecessor-version":[{"id":367,"href":"https:\/\/mizar-jp.org\/index.php?rest_route=\/wp\/v2\/pages\/23\/revisions\/367"}],"wp:attachment":[{"href":"https:\/\/mizar-jp.org\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=23"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}