{"id":19,"date":"2019-09-02T04:09:45","date_gmt":"2019-09-02T04:09:45","guid":{"rendered":"http:\/\/mizar-jp.org\/?page_id=19"},"modified":"2020-11-05T21:39:01","modified_gmt":"2020-11-05T12:39:01","slug":"%e8%a8%ad%e7%ab%8b%e4%b8%bb%e6%97%a8","status":"publish","type":"page","link":"https:\/\/mizar-jp.org\/?page_id=19","title":{"rendered":"\u8a2d\u7acb\u4e3b\u65e8"},"content":{"rendered":"\n<figure class=\"wp-block-image size-large\"><img loading=\"lazy\" decoding=\"async\" width=\"1024\" height=\"397\" src=\"http:\/\/mizar-jp.org\/wp-content\/uploads\/2020\/11\/grid-871475_1280w-1024x397.jpg\" alt=\"\" class=\"wp-image-243\" srcset=\"https:\/\/mizar-jp.org\/wp-content\/uploads\/2020\/11\/grid-871475_1280w-1024x397.jpg 1024w, https:\/\/mizar-jp.org\/wp-content\/uploads\/2020\/11\/grid-871475_1280w-300x116.jpg 300w, https:\/\/mizar-jp.org\/wp-content\/uploads\/2020\/11\/grid-871475_1280w-768x298.jpg 768w, https:\/\/mizar-jp.org\/wp-content\/uploads\/2020\/11\/grid-871475_1280w.jpg 1280w\" sizes=\"auto, (max-width: 1024px) 100vw, 1024px\" \/><\/figure>\n\n\n\n<p>\u3000\u6570\u5b66\u306f\u304b\u3064\u3066\u79d1\u5b66\u306b\u304a\u3051\u308b\u5973\u738b\u306e\u3088\u3046\u306a\u7acb\u5834\u306b\u3042\u308a\u307e\u3057\u305f\u3002\u30ac\u30a6\u30b9\u306e\u3088\u3046\u306b\u3001\u6570\u5b66\u8005\u306f\u540c\u6642\u306b\u79d1\u5b66\u8005\u3067\u3042\u308a\u307e\u305f\u5929\u6587\u5b66\u8005\u3067\u3082\u3042\u308a\u307e\u3057\u305f\u3002\u30cb\u30e5\u30fc\u30c8\u30f3\u306f\u30e9\u30a4\u30d7\u30cb\u30c3\u30c4\u3068\u4e26\u3093\u3067\u5fae\u7a4d\u5206\u5b66\u306e\u5275\u59cb\u8005\u3067\u3042\u308b\u3068\u540c\u6642\u306b\u52ff\u8ad6\u3001\u529b\u5b66\u306e\u7956\u3067\u3082\u3042\u308a\u307e\u3059\u3002\u3057\u304b\u305720\u4e16\u7d00\u306b\u306a\u3063\u3066\u516c\u7406\u4e3b\u7fa9\u304c\u529b\u3092\u6301\u3064\u3068\u540c\u6642\u306b\uff08\u305d\u308c\u306f\u76f8\u5bfe\u6027\u7406\u8ad6\u306a\u3069\u65b0\u3057\u3044\u7269\u7406\u5b66\u306b\u9069\u5207\u306a\u6570\u5b66\u3092\u63d0\u4f9b\u3067\u304d\u305f\u3001\u3068\u3044\u3046\u529f\u7e3e\u306f\u3042\u308a\u307e\u3057\u305f\u304c\uff09\u3001\u6570\u5b66\u8005\u306e\u6570\u3060\u3051\u516c\u7406\u7cfb\u304c\u3042\u308b\u3001\u3068\u3044\u3046\u3088\u3046\u306a\u72b6\u6cc1\u306b\u306a\u308a\u3001\u6570\u5b66\u306f\u767a\u6563\u3068\u5b64\u72ec\u5316\u306e\u9053\u3092\u6b69\u307f\u59cb\u3081\u307e\u3059\u3002\u5f53\u7136\u306e\u3088\u3046\u306b\u79d1\u5b66\u8005\u3084\u5de5\u5b66\u8005\u306f\u73fe\u4ee3\u6570\u5b66\u3092\u7406\u89e3\u3067\u304d\u306a\u304f\u306a\u308a\u3001\u305d\u3057\u3066\u6570\u5b66\u3092\u7121\u8996\u3057\u306f\u3058\u3081\u307e\u3059\u3002\u305d\u308c\u304c\u73fe\u4ee3\u6570\u5b66\u306e\u75c5\u56e0\u3060\u3068\u8003\u3048\u3089\u308c\u307e\u3059\u3002\u3057\u304b\u3057\u4ed6\u65b9\u3001\uff12\uff11\u4e16\u7d00\u306b\u306a\u308a\u3001\u30b3\u30f3\u30d4\u30e5\u30fc\u30bf\u5316\u3057\u305f\u6642\u4ee3\u306b\u306f\u3001\u76ca\u3005\u9ad8\u5ea6\u306e\u6570\u5b66\u304c\u8981\u6c42\u3055\u308c\u307e\u3059\u3002<\/p>\n\n\n\n<p>\u3000\u79c1\u306e\u5927\u5b66\u3067\u306e\u6069\u5e2b\u6885\u57a3\u5bff\u6625\u6559\u6388\u306f\u3001\u300c\u7b2c\u4e00\u6b21\u5927\u6226\u306f\u5316\u5b66\u306e\u6226\u4e89\u3067\u3042\u3063\u305f\u3002\u706b\u85ac\u3001\u6bd2\u30ac\u30b9\u3001\u306a\u3069\u306f\u5316\u5b66\u306e\u7523\u7269\u3067\u3042\u308b\u3002\u7b2c\u4e8c\u6b21\u5927\u6226\u306f\u7269\u7406\u5b66\u306e\u6226\u4e89\u3067\u3042\u3063\u305f\u3002\u822a\u7a7a\u6a5f\u3001\u30ec\u30fc\u30c0\u3001\u539f\u7206\u306a\u3069\u306f\u7269\u7406\u5b66\u306e\u7523\u7269\u3067\u3042\u308b\u3002\u3082\u3057\u3053\u308c\u304b\u3089\u7b2c\u4e09\u6b21\u5927\u6226\u304c\u8d77\u304d\u308c\u3070\uff08\u8d77\u304d\u3066\u306f\u56f0\u308b\u304c\uff09\u305d\u308c\u306f\u6570\u5b66\u306e\u6226\u4e89\u3067\u3042\u308d\u3046\u300d\u3001\u3068\u65e5\u9803\u8a71\u3057\u3066\u304a\u3089\u308c\u307e\u3057 \u305f\u3002\u305d\u308c\u306f\u4f55\u5341\u5e74\u3082\u524d\u306e\u8a71\u306a\u306e\u3067\u3001\u305d\u3093\u306a\u3053\u3068\u304c\u3042\u308a\u5f97\u308b\u306e\u3060\u308d\u3046\u304b\u3001\u3068\u79c1\u306f\u7591\u554f\u306b\u601d\u3044\u306a\u304c\u3089\u805e\u3044\u3066\u3044\u305f\u3082\u306e\u3067\u3059\u3002<\/p>\n\n\n\n<p>\u3000\u3057\u304b\u3057\u30b3\u30f3\u30d4\u30e5\u30fc\u30bf\u306e\u767a\u9054\u3057\u305f\u73fe\u4ee3\u3067\u306f\u305d\u308c\u306f\u771f\u5b9f\u5473\u3092\u5e2f\u3073\u3066\u3044\u307e\u3059\u3002\u30df\u30b5\u30a4\u30eb\u306f\u512a\u308c\u305f\u30ca\u30d3\u30b2\u30fc\u30b7\u30e7\u30f3\u30bd\u30d5\u30c8\u306b\u3088\u3063\u3066\u5236\u5fa1\u3055\u308c\u3066\u3044\u307e\u3059\u3002\u6697\u53f7\u306f\u9ad8\u5ea6\u306e\u4ee3\u6570\u5b66\u3092\u4f7f\u3063\u3066\u4f5c\u3089\u308c\u307e\u3059\u3002\u30ed\u30dc\u30c3\u30c8\u5175\u5668\u306f\u4eba\u5de5\u77e5\u80fd\u30bd\u30d5\u30c8\u306b\u3088\u3063\u3066\u52d5\u304b\u3055\u308c\u3066\u3044\u307e\u3059\u3002\u7b2c\u4e09\u6b21\u5927\u6226\u306a\u3069\u8d77\u304d\u306a\u3044\u3068\u3057\u3066\u3082\u3001\u56fd\u969b\u7684\u306a\u7d4c\u6e08\u6226\u4e89\u306f\u3084\u306f\u308a\u3001\u6570\u5b66\u3092\u5229\u7528\u3057\u305f\u9ad8\u5ea6\u306e\u30b3\u30f3\u30d4\u30e5\u30fc\u30bf\u30b7\u30b9\u30c6\u30e0\u304c\u4e3b\u5f79\u306b\u306a\u308b\u3067\u3057\u3087\u3046\u3002<\/p>\n\n\n\n<p>\u3000\u30b3\u30f3\u30d4\u30e5\u30fc\u30bf\u306f\u3001\u9ad8\u5ea6\u304b\u3064\u7cbe\u7dfb\u306a\u6570\u5b66\u306e\u8981\u6c42\u8005\u3067\u3042\u308b\u3068\u540c\u6642\u306b\u3001\u305d\u306e\u3088\u3046\u306a\u65b0\u3057\u3044\u6570\u5b66\u624b\u6cd5\u306e\u751f\u307f\u306e\u89aa\u3067\u3082\u3042\u308b\u306e\u3067\u3059\u3002\u5373\u3061\u3001\u30d7\u30eb\u30fc\u30d5\u30c1\u30a7\u30c3\u30ab\u30fc\u3068\u6570\u5b66\u8a00\u8a9e\u306e\u51fa\u73fe\u3092\u53ef\u80fd\u306b\u3057\u307e\u3057\u305f\u3002\u3082\u3063\u3068\u7aef\u7684\u306b\u8a00\u3048\u3070Mizar\u306e\u51fa\u73fe\u3092\u53ef\u80fd\u306b\u3057\u305f\u306e\u3067\u3059\u3002Mizar\u306f\u30dd\u30fc\u30e9\u30f3\u30c9\u306eTrybulec\u5148\u751f\u304c\u4e2d\u5fc3\u306b\u306a\u3063\u3066\u958b\u767a\u3055\u308c\u305f\u30b7\u30b9\u30c6\u30e0\u3067\u3059\u3002Mizar\u8a00\u8a9e\u3067\u66f8\u304b\u308c\u305f\u6570\u5b66\u7406\u8ad6\u306f\u3001Mizar\u306e\u30c1\u30a7\u30c3\u30ab\u30fc\u30bd \u30d5\u30c8\uff08verifier\uff09\u306b\u3088\u3063\u3066\u305d\u306e\u6b63\u3057\u3055\u304c\u81ea\u52d5\u7684\u306b\u30c1\u30a7\u30c3\u30af\u3055\u308c\u307e\u3059\u3002\u30c1\u30a7\u30c3\u30af\u3092\u901a\u3063\u305f\u7406\u8ad6\u306f\uff08\u305d\u306e\u4ed6\u306e\u30c1\u30a7\u30c3\u30af\u3082\u3042\u308a\u307e\u3059\u304c\uff09\u30a4\u30f3\u30bf\u30fc\u30cd\u30c3\u30c8\u306e\u30b5\u30fc \u30d0\u306b\u7f6e\u304b\u308c\uff08Mizar\u3000Mathematical\u3000Library\u3001MML\uff09\u3001\u4eba\u985e\u5171\u6709\u306e\u77e5\u7684\u8ca1\u7523\u3068\u3057\u3066\u4e16\u754c\u306b\u516c\u958b\u3055\u308c\u307e\u3059\u3002<\/p>\n\n\n\n<p>\u3000Mizar\u306e\u77e5\u7684\u8ca1\u7523\u306f\u4e0d\u601d\u8b70\u306a\u6027\u683c\u3092\u6301\u3063\u3066\u3044\u307e\u3059\u3002\u8ab0\u3067\u3082\u304c\uff08\u56fd\u7c4d\u3001\u8ca7\u5bcc\u3001\u6027\u5225\u3001\u5e74\u9f62\u3001\u968e\u7d1a\u306a\u3069\u306b\u7121\u95a2\u4fc2\u306b\uff09\u53ea\u3067\u5165\u624b\u53ef\u80fd\u306a\u3001\u516c\u5e73\u306a\u8ca1\u7523\u3067\u3059\u3002\u3067\u3082\u305d\u308c\u3092\u91cd\u8981\u8996\u3057\u306a\u3044\u4eba\u3005\u306b\u3068\u3063\u3066\u306f\u4f55\u306e\u826f\u3044\u3053\u3068\u3082\u3042\u308a\u307e\u305b\u3093\u3002\u3057\u304b\u3057\u91cd\u8981\u8996\u3059\u308b\u4eba\u3005\u306b\u306f\u529b\u3084\u5bcc\u3084\u7e41\u6804\u3092\u4e0e\u3048\u308b\u3053\u3068\u304c\u3067\u304d\u307e\u3059\u3002Mizar\u30e9\u30a4\u30d6\u30e9\u30ea\u30fc\u3078\u306e\u65e5\u672c\u306e\u8ca2\u732e\u306f\u5927\u304d\u306a\u3082\u306e\u304c\u3042\u308a\u307e\u3059\u3002\u3053\u308c\u306f\u6700\u3082\u5d07\u9ad8\u306a\u30dc\u30e9\u30f3\u30c6\u30a3\u30a2\u7684\u6d3b\u52d5\u3067\u3042\u308a\u4e16\u754c\u306b\u8ca2\u732e\u3059\u308b\u3068\u540c\u6642\u306b\u3001\u65e5\u672c\u81ea\u8eab\u306e\u79d1\u5b66\u6280\u8853\u306e\u6c34\u6e96\u3092\u30c8\u30c3\u30d7\u30e9\u30f3\u30af\u306b\u62bc\u3057\u4e0a\u3052\u3046\u308b\u3082\u306e\u3067\u3059\u3002Mizar\u306e\u65e5\u672c\u306b\u65bc\u3051\u308b\u6d3b\u52d5\u304c\u76ca\u3005\u91cd\u8981\u306b\u306a\u308b\u306b\u3064\u308c\u3001\u65e5\u672c\u306b\u65bc\u3051\u308b\u7814\u7a76\u8005\u304c\u3082\u3046\u5c11\u3057\u7d44\u7e54\u5316\u3055\u308c\u3066\u3001\u793e\u4f1a\u306b\u5f71\u97ff\u3092\u53ca\u307c\u305b\u308b\u5f62\u306b\u3059\u3079\u304d\u3068\u8003\u3048\u307e\u3059\u3002<\/p>\n\n\n\n<p>\u3000\u305d\u308c\u304c\u300c\u65e5\u672cMizar\u5b66\u4f1a\u300d\u8a2d\u7acb\u306e\u4e3b\u65e8\u3067\u3042\u308a\u307e\u3059\u3002\u3053\u306e\u5b66\u4f1a\u306f\u5358\u306bMML\u3092\u5897\u3084\u3059\u6d3b\u52d5\u3060\u3051\u3067\u306a\u304f\u3001\u30ac\u30a6\u30b9\u306e\u6642\u4ee3\u306e\u3088\u3046\u306b\u9ad8\u5ea6\u306a\u65b0\u3057\u3044\u6570\u5b66\u304c\u3001\u79d1\u5b66\u3084\u6280\u8853\u3084\u7523\u696d\u306b\u91cd\u8981\u306a\u5f71\u97ff\u3092\u53ca\u307c\u305b\u308b\u3088\u3046\u306a\u6d3b\u52d5\u3082\u3057\u3066\u3086\u304d\u307e\u3059\u3002\u3053\u306e\u5b66\u4f1a\u3092\u57fa\u76e4\u306b\u3057\u3066\u3001\u500b\u3005\u306e\u7814\u7a76\u8005\u306f\u751f\u304d\u751f\u304d\u3068\u3057\u305f\u6d3b\u52d5\u3092\u59cb\u3081\u3089\u308c\u308b\u3053\u3068\u3067\u3057\u3087\u3046\u3002<\/p>\n\n\n\n<p class=\"has-text-align-right\">2007\u5e745\u67081\u65e5\u3000\u3000\u4e2d\u6751\u516b\u675f<\/p>\n","protected":false},"excerpt":{"rendered":"<p>\u3000\u6570\u5b66\u306f\u304b\u3064\u3066\u79d1\u5b66\u306b\u304a\u3051\u308b\u5973\u738b\u306e\u3088\u3046\u306a\u7acb\u5834\u306b\u3042\u308a\u307e\u3057\u305f\u3002\u30ac\u30a6\u30b9\u306e\u3088\u3046\u306b\u3001\u6570\u5b66\u8005\u306f\u540c\u6642\u306b\u79d1\u5b66\u8005\u3067\u3042\u308a\u307e\u305f\u5929\u6587\u5b66\u8005\u3067\u3082\u3042\u308a\u307e\u3057\u305f\u3002\u30cb\u30e5\u30fc\u30c8\u30f3\u306f\u30e9\u30a4\u30d7\u30cb\u30c3\u30c4\u3068\u4e26\u3093\u3067\u5fae\u7a4d\u5206\u5b66\u306e\u5275\u59cb\u8005\u3067\u3042\u308b\u3068\u540c\u6642\u306b\u52ff\u8ad6\u3001\u529b\u5b66\u306e\u7956\u3067\u3082\u3042\u308a\u307e\u3059\u3002\u3057\u304b [&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-19","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/mizar-jp.org\/index.php?rest_route=\/wp\/v2\/pages\/19","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=19"}],"version-history":[{"count":7,"href":"https:\/\/mizar-jp.org\/index.php?rest_route=\/wp\/v2\/pages\/19\/revisions"}],"predecessor-version":[{"id":245,"href":"https:\/\/mizar-jp.org\/index.php?rest_route=\/wp\/v2\/pages\/19\/revisions\/245"}],"wp:attachment":[{"href":"https:\/\/mizar-jp.org\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=19"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}