Reseña: Hofstadter’s problem for curious readers

Se ha publicado un artículo de razonamiento formalizado en Coq titulado Hofstadter’s problem for curious readers.

Su autor es Pierre Letouzey (del grupo PPS (Preuves, Programmes et Systèmes) de la Universidad de París VII Denis Diderot, Francia).

Su resumen es

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ödel, Escher, Bach” 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 in OEIS, while the flipped version is the sequence A123070.

The detailed and machine-checked proofs can be found in the files of
this development 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 “Coq-to-English” 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.

El código de las correspondientes teorías en Coq se encuentra aquí.

Este artículo puede servir de lectura complementaria en los cursos de Razonamiento automático, Razonamiento asistido por ordenador y Lógica computacional y teoría de modelos.