{"id":5025,"date":"2015-09-16T07:14:28","date_gmt":"2015-09-16T05:14:28","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=5025"},"modified":"2015-09-16T07:14:28","modified_gmt":"2015-09-16T05:14:28","slug":"resena-hofstadters-problem-for-curious-readers","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-hofstadters-problem-for-curious-readers\/","title":{"rendered":"Rese\u00f1a: Hofstadter’s problem for curious readers"},"content":{"rendered":"

Se ha publicado un art\u00edculo de razonamiento formalizado en Coq<\/a> titulado Hofstadter’s problem for curious readers<\/a>.<\/p>\n

Su autor es Pierre Letouzey<\/a> (del grupo PPS (Preuves, Programmes et Syst\u00e8mes)<\/a> de la Universidad de Par\u00eds VII Denis Diderot<\/a>, Francia).<\/p>\n

Su resumen es<\/p>\n

\n This document summarizes the proofs made during a Coq development in Summer 2015. This development investigates the function G introduced by Hofstadter in his famous “G\u00f6del, Escher, Bach”<\/a> book as well as a related infinite tree. The left\/right flipped variant of this G tree has also been studied here, following Hofstadter’s “problem for the curious reader”. The initial G function is refered as sequence A005206<\/a> in OEIS, while the flipped version is the sequence A123070<\/a>.<\/p>\n

The detailed and machine-checked proofs can be found in the files of
\n this development<\/a> and can be re-checked by running Coq version 8.4 on it. No prior knowledge of Coq is assumed here, on the contrary this document has rather been a \u201cCoq-to-English\u201d translation exercise for the author. Nonetheless, some proofs given in this document are still quite sketchy: in this case, the interested reader is encouraged to consult the Coq files given as references.\n<\/p><\/blockquote>\n

El c\u00f3digo de las correspondientes teor\u00edas en Coq se encuentra aqu\u00ed<\/a>.<\/p>\n

Este art\u00edculo puede servir de lectura complementaria en los cursos de Razonamiento autom\u00e1tico<\/a>, Razonamiento asistido por ordenador<\/a> y L\u00f3gica computacional y teor\u00eda de modelos<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"

Se ha publicado un art\u00edculo de razonamiento formalizado en Coq titulado Hofstadter’s problem for curious readers. Su autor es Pierre Letouzey (del grupo PPS (Preuves, Programmes et Syst\u00e8mes) de la Universidad de Par\u00eds VII Denis Diderot, Francia). Su resumen es This document summarizes the proofs made during a Coq development in Summer 2015. This development…<\/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":[45,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\/5025"}],"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=5025"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5025\/revisions"}],"predecessor-version":[{"id":5026,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5025\/revisions\/5026"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=5025"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=5025"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=5025"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}