{"id":3473,"date":"2013-08-07T14:54:45","date_gmt":"2013-08-07T14:54:45","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3473"},"modified":"2013-08-07T14:54:45","modified_gmt":"2013-08-07T14:54:45","slug":"the-konigsberg-bridge-problem-and-the-friendship-theorem","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/the-konigsberg-bridge-problem-and-the-friendship-theorem\/","title":{"rendered":"The K\u00f6nigsberg bridge problem and the friendship 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\/index.html\">Isabelle\/HOL<\/a> titulado <a href=\"http:\/\/afp.sourceforge.net\/entries\/Koenigsberg_Friendship.shtml\">The K\u00f6nigsberg bridge problem and the friendship theorem<\/a>.<\/p>\n<p>Su autor es Wenda Li (de la Universidad de Cambridge).<\/p>\n<p>El art\u00edculo se ha publicado el 17 de julio en el <a href=\"http:\/\/afp.sourceforge.net\/index.shtml\">Archive of Formal Proofs<\/a>. <\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\nThis development provides a formalization of undirected graphs and simple graphs, which are based on Benedikt Nordhoff and Peter Lammich&#8217;s simple formalization of labelled directed graphs in the archive. Then, with our formalization of graphs, we show both necessary and sufficient conditions for Eulerian trails and circuits as well as the fact that the K\u00f6nigsberg Bridge Problem does not have a solution. In addition, we show the Friendship Theorem in simple graphs.\n<\/p><\/blockquote>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Isabelle\/HOL titulado The K\u00f6nigsberg bridge problem and the friendship theorem. Su autor es Wenda Li (de la Universidad de Cambridge). El art\u00edculo se ha publicado el 17 de julio en el Archive of Formal Proofs. Su resumen es This development provides a formalization of undirected graphs&#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":[1],"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\/3473"}],"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=3473"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3473\/revisions"}],"predecessor-version":[{"id":3474,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3473\/revisions\/3474"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3473"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3473"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3473"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}