{"id":2155,"date":"2012-08-31T07:13:16","date_gmt":"2012-08-31T07:13:16","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=2155"},"modified":"2013-03-08T05:48:12","modified_gmt":"2013-03-08T05:48:12","slug":"formalization-and-verification-of-number-theoretic-algorithms-using-the-mizar-proof-checker","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/formalization-and-verification-of-number-theoretic-algorithms-using-the-mizar-proof-checker\/","title":{"rendered":"Rese\u00f1a: Formalization and verification of number theoretic algorithms using the Mizar proof checker"},"content":{"rendered":"<p>En el <a href=\"http:\/\/www.world-academy-of-science.org\/worldcomp12\/ws\/conferences\/fcs12\">FCS&#8217;12<\/a> (<i>The 2012 International Conference on Foundations of Computer Science<\/i>) se present\u00f3 un trabajo de razonamiento formalizado en <a href=\"http:\/\/mizar.org\/project\">Mizar<\/a> titulado <a href=\"http:\/\/elrond.informatik.tu-freiberg.de\/papers\/WorldComp2012\/FCS2680.pdf\">Formalization and verification of number theoretic algorithms using the Mizar proof checker<\/a>.<\/p>\n<p>Sus autores son <a href=\"http:\/\/www.informatik.uni-trier.de\/~ley\/db\/indices\/a-tree\/o\/Okazaki:Hiroyuki.html\">Hiroyuki Okazaki<\/a>, Yoshiki Aoki y <a href=\"http:\/\/soar-rd.shinshu-u.ac.jp\/profile\/en.OeceZVkh.html\">Yasunari Shidama<\/a> (de la <i>Shinshu University<\/i>).<\/p>\n<p>Su resumen es <\/p>\n<blockquote><p>\nIn this paper, we introduce formalization of well-known number theoretic algorithms on the <a href=\"http:\/\/mizar.org\">Mizar<\/a> proof checking system. We formalized the Euclidean algorithm, the extended Euclidean algorithm and the algorithm computing the solution of the Chinese reminder theorem based on the source code of <a href=\"http:\/\/tnt.math.se.tmu.ac.jp\/nzmath\/index.html\">NZMATH<\/a> which is a Python based number theory oriented calculation system. We prove the accuracy of our formalization using the Mizar proof checking system as a formal verification tool.\n<\/p><\/blockquote>\n","protected":false},"excerpt":{"rendered":"<p>En el FCS&#8217;12 (The 2012 International Conference on Foundations of Computer Science) se present\u00f3 un trabajo de razonamiento formalizado en Mizar titulado Formalization and verification of number theoretic algorithms using the Mizar proof checker. Sus autores son Hiroyuki Okazaki, Yoshiki Aoki y Yasunari Shidama (de la Shinshu University). Su resumen es In this paper, we&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[100],"tags":[188,273,285],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2155"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=2155"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2155\/revisions"}],"predecessor-version":[{"id":2785,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2155\/revisions\/2785"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=2155"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=2155"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=2155"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}