{"id":3599,"date":"2013-09-09T07:40:34","date_gmt":"2013-09-09T05:40:34","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3599"},"modified":"2013-09-09T07:42:03","modified_gmt":"2013-09-09T05:42:03","slug":"computer-theorem-proving-and-hott","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/computer-theorem-proving-and-hott\/","title":{"rendered":"Computer theorem proving and HoTT"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo sobre la demostraci\u00f3n asistida por ordenador y los fundamentos de la matem\u00e1tica titulado <a href=\"http:\/\/centaur.reading.ac.uk\/33158\/1\/HoTT.pdf\">Computer theorem proving and HoTT<\/a>.<\/p>\n<p>Sus autores son <a href=\"http:\/\/www.gilith.com\/\">Joe Leslie-Hurd<\/a> (de <i>Intel Corporation<\/i>) y <a href=\"http:\/\/www.reading.ac.uk\/sse\/about\/staff\/g-haworth.aspx\">G. McC. Haworth<\/a> (de la Universidad de Reading).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\n<a href=\"http:\/\/en.wikipedia.org\/wiki\/Automated_theorem_proving\">Theorem-proving<\/a> is a one-player game. The history of computer programs being the players goes back to 1956 and the <a href=\"http:\/\/en.wikipedia.org\/wiki\/Logic_Theorist\">&#8216;LT&#8217; Logic Theory Machine<\/a> of Newell, Shaw and Simon. In game-playing terms, the &#8216;initial position&#8217; is the core set of axioms chosen for the particular logic and the &#8216;moves&#8217; are the rules of inference. Now, the <a href=\"http:\/\/www.math.ias.edu\/sp\/univalent\/goals\">Univalent Foundations Program<\/a> at IAS Princeton and the resulting <a href=\"http:\/\/homotopytypetheory.org\/book\/\">&#8216;HoTT&#8217; book on Homotopy Type Theory<\/a> have demonstrated the success of a new kind of experimental mathematics using computer theorem proving.\n<\/p><\/blockquote>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo sobre la demostraci\u00f3n asistida por ordenador y los fundamentos de la matem\u00e1tica titulado Computer theorem proving and HoTT. Sus autores son Joe Leslie-Hurd (de Intel Corporation) y G. McC. Haworth (de la Universidad de Reading). Su resumen es Theorem-proving is a one-player game. The history of computer programs being the&#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":[218,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\/3599"}],"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=3599"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3599\/revisions"}],"predecessor-version":[{"id":3601,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3599\/revisions\/3601"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3599"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3599"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3599"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}