{"id":3874,"date":"2013-12-02T07:29:31","date_gmt":"2013-12-02T06:29:31","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3874"},"modified":"2013-12-02T07:30:24","modified_gmt":"2013-12-02T06:30:24","slug":"certified-kruskals-tree-theorem","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/certified-kruskals-tree-theorem\/","title":{"rendered":"Certified Kruskal\u2019s tree theorem"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/\">Isabelle\/HOL<\/a> sobre \u00f3rdenes titulado  <a href=\"http:\/\/cl-informatik.uibk.ac.at\/users\/griff\/publications\/Sternagel-CPP13.pdf\">Certified Kruskal\u2019s tree theorem<\/a>.<\/p>\n<p>Su autor es <a href=\"http:\/\/www.jaist.ac.jp\/~c-sterna\">Christian Sternagel<\/a> (del <i>Japan Advanced Institute of Science and Technology<\/i>).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\nThis paper gives the first formalization of Kruskal\u2019s tree theorem in a proof assistant. More concretely, an Isabelle\/HOL development of Nash-Williams\u2019 minimal bad sequence argument for proving the tree theorem is presented. Along the way, the proofs of Dickson\u2019s lemma and Higman\u2019s lemma are discussed.\n<\/p><\/blockquote>\n<p>El trabajo se presentar\u00e1 en el <a href=\"http:\/\/cpp2013.forge.nicta.com.au\/\">CPP 2013<\/a> (<i>3rd International Conference on Certified Programs and Proofs<\/i>).<\/p>\n<p>El c\u00f3digo de las correspondientes teor\u00edas en Isabelle\/HOL se encuentra <a href=\"http:\/\/afp.sourceforge.net\/devel-entries\/Well_Quasi_Orders.shtml\">aqu\u00ed<\/a>. <\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Isabelle\/HOL sobre \u00f3rdenes titulado Certified Kruskal\u2019s tree theorem. Su autor es Christian Sternagel (del Japan Advanced Institute of Science and Technology). Su resumen es This paper gives the first formalization of Kruskal\u2019s tree theorem in a proof assistant. More concretely, an Isabelle\/HOL development of Nash-Williams\u2019 minimal&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","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":[144,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\/3874"}],"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=3874"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3874\/revisions"}],"predecessor-version":[{"id":3876,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3874\/revisions\/3876"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3874"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3874"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3874"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}