Coq

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.

Se ha publicado un artículo de razonamiento formalizado en Coq sobre codificación titulado Formalization of error-correcting codes (from Hamming to modern coding theory)

Sus autores son

• Reynald Affeldt (del AIST (National Institute of Advanced Industrial Science and Technology) en Tsukuba, Japón) y
• Jacques Garrigue (de la Universidad de Nagoya en Nagoya, Japón).

Su resumen es

By adding redundancy to transmitted data, error-correcting codes (ECCs) make it possible to communicate reliably over noisy channels. Minimizing redundancy and (de)coding time has driven much research, culminating with Low-Density Parity-Check (LDPC) codes. At first sight, ECCs may be considered as a trustful piece of computer systems because classical results are well-understood. But ECCs are also performance-critical so that new hardware calls for new implementations whose testing is always an issue. Moreover, research about ECCs is still flourishing with papers of ever-growing complexity. In order to provide means for implementers to perform verification and for researchers to firmly assess recent advances, we have been developing a formalization of ECCs using the SSReflect extension of the Coq proof-assistant. We report on the formalization of linear ECCs, duly illustrated with a theory about the celebrated Hamming codes and the verification of the sum-product algorithm for decoding LDPC codes.

El trabajo se presentó el 25 de agosto en el ITP 2015 (The 6th conference on Interactive Theorem Proving).

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.

Se ha publicado un artículo de aplicación del razonamiento asistido por ordenador a la enseñanza titulado TryLogic tutorial: An approach to learning Logic by proving and refuting

Sus autores son Patrick Terrematte y João Marcos (del Group for Logic, Language, Information, Theory and Applications (LoLITA) en la Federal University of Rio Grande do Norte (UFRN) de Brasil).

Su resumen es

Aiming to offer a framework for blended learning to the teaching of proof theory, the present paper describes an interactive tutorial, called TryLogic, teaching how to solve logical conjectures either by proofs or refutations. The paper also describes the integration of our infrastructure with the Virtual Learning Environment Moodle through the IMS Learning Tools Interoperability specification, and evaluates the tool we have developed.

El trabajo se ha presentado en TTL2015 (Fourth International Conference on Tools for Teaching Logic)

Se ha publicado un artículo de razonamiento formalizado en Coq titulado Formal study of functional orbits in finite domains.

Su autor es Jean-François Dufourd (del grupo Computer Science in Geometry and Graphics (IGG) en la Univ. de Estrasburgo, Francia).

Su resumen es

In computer science, functional orbits − i.e tracks left by iterating a function − in a finite domain naturally appear at a high or a low level. This paper introduces a Coq logical orbit framework, the purpose of which is to help rigorously developing software systems with some complex data structures from specification to implementation.

The result is a Coq library of orbit concepts formalized as definitions, lemmas and theorems. Most of them are inspired by our previous work in geometric modelling, where combinatorial hypermaps were used to describe surface subdivisions appearing in computational geometry problems, e.g. building convex hulls or Delaunay diagrams. Now, this domain remains a reference for us, but our results are drastically extended and usable in other computer science areas. The proof of Floyd’s cycle-detection algorithm, known as “the tortoise and the hare”, confirms that point.

The library contains operations to observe, traverse and update orbits − addition, deletion, mutation, transposition − with proofs of their behavior. It focuses on the important case where the involved function is a partial injection. In this case, it defines a connectivity relationship and evaluates the variation of the number of connected components during updates.

El trabajo se ha publicado en Theoretical Computer Science.