{"id":4359,"date":"2014-07-08T08:24:58","date_gmt":"2014-07-08T06:24:58","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4359"},"modified":"2014-07-08T08:26:05","modified_gmt":"2014-07-08T06:26:05","slug":"resena-cardinals-in-isabellehol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-cardinals-in-isabellehol\/","title":{"rendered":"Rese\u00f1a: Cardinals in Isabelle\/HOL"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en  <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/index.html\">Isabelle\/HOL<\/a> sobre teor\u00eda de conjuntos titulado <a href=\"http:\/\/bit.ly\/1k19vXC\">Cardinals in Isabelle\/HOL<\/a>.<\/p>\n<p>Sus autores son <a href=\"http:\/\/www4.in.tum.de\/~blanchet\">Jasmin Christian Blanchette<\/a>, <a href=\"http:\/\/www4.in.tum.de\/~popescua\">Andrei Popescu<\/a> y <a href=\"http:\/\/www21.in.tum.de\/~traytel\">Dmitriy Traytel<\/a> (de la Univ. T\u00e9cnica de Munich).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\n  <em>We report on a formalization of ordinals and cardinals in Isabelle\/HOL. A main challenge we faced is the inability of higher-order logic to represent ordinals canonically, as transitive sets (as done in set theory). We resolved this into a \u201cdecentralized\u201d representation that identifies ordinals with wellorders, with all concepts and results proved to be invariant under order isomorphism. We also discuss two applications of this general theory in formal developments.<\/em>\n<\/p><\/blockquote>\n<p>El trabajo se presentar\u00e1 el martes 15 de julio en el <a href=\"http:\/\/www.cs.uwyo.edu\/~ruben\/itp-2014\">ITP 2014<\/a> (<em>5th Conference on Interactive Theorem Proving<\/em>).<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Isabelle\/HOL sobre teor\u00eda de conjuntos titulado Cardinals in Isabelle\/HOL. Sus autores son Jasmin Christian Blanchette, Andrei Popescu y Dmitriy Traytel (de la Univ. T\u00e9cnica de Munich). Su resumen es We report on a formalization of ordinals and cardinals in Isabelle\/HOL. A main challenge we faced is&#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\/4359"}],"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=4359"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4359\/revisions"}],"predecessor-version":[{"id":4361,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4359\/revisions\/4361"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4359"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4359"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4359"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}