{"id":5451,"date":"2016-05-24T06:20:45","date_gmt":"2016-05-24T04:20:45","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=5451"},"modified":"2016-05-24T06:21:52","modified_gmt":"2016-05-24T04:21:52","slug":"resena-compass-free-navigation-of-mazes","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-compass-free-navigation-of-mazes\/","title":{"rendered":"Rese\u00f1a: Compass-free navigation of mazes"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"http:\/\/www.cl.cam.ac.uk\/~jrh13\/hol-light\">HOL Light<\/a> sobre geometr\u00eda titulado <a href=\"http:\/\/www.research.ed.ac.uk\/portal\/files\/25192549\/Compass_free_Navigation_of_Mazes.pdf\">Compass-free navigation of mazes<\/a><\/p>\n<p>Sus autores son <a href=\"https:\/\/www.inf.ed.ac.uk\/people\/staff\/Phil_Scott.html\">Phil Scott<\/a> y <a href=\"http:\/\/homepages.inf.ed.ac.uk\/jdf\/\">Jacques Fleuriot<\/a> (de la Universidad de Edimburgo).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\n  If you find yourself in a corridor of a standard maze, a sure and easy way to  escape is to simply pick the left (or right) wall, and then follow it along its twists and turns  and around the dead-ends till you eventually arrive at the exit. But what happens when you cannot tell left from right? What if you cannot tell North from South? What if you cannot judge distances, and have no idea what it means to follow a wall in a given direction? The possibility of escape in these circumstances is suggested in the statement of an unproven theorem given in David Hilbert\u2019s celebrated Foundations of Geometry, in which he effectively claimed that a standard maze could be fully navigated using axioms and concepts based solely on the relations of points lying on lines in a specified order. We discuss our algorithm for this surprisingly challenging version of the maze navigation problem, and our HOL Light verification of its correctness from Hilbert\u2019s axioms.\n<\/p><\/blockquote>\n<p>El trabajo se ha presentado en el <a href=\"http:\/\/www.i-eos.com\/index.php\">SCSS 2016<\/a> (<em>7th International Symposium on Symbolic Computation in Software Science<\/em>).<\/p>\n<p>El c\u00f3digo de las correspondientes teor\u00edas en HOL Light se encuentra <a href=\"https:\/\/github.com\/Chattered\/hilbert-bundle\/tree\/master\/hol-light\/hilbert\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en HOL Light sobre geometr\u00eda titulado Compass-free navigation of mazes Sus autores son Phil Scott y Jacques Fleuriot (de la Universidad de Edimburgo). Su resumen es If you find yourself in a corridor of a standard maze, a sure and easy way to escape is to simply&#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":[22,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\/5451"}],"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=5451"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5451\/revisions"}],"predecessor-version":[{"id":5453,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5451\/revisions\/5453"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=5451"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=5451"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=5451"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}