Día: 12 agosto 2015

Se ha publicado un artículo de razonamiento formalizado en Coq sobre la aritmética titulado Formal verification of programs computing the floating-point average.

Sus autora es Silvie Boldo (del grupo Toccata (Formally Verified Programs, Certified Tools and Numerical Computations) en el LRI (Laboratoire de Recherche en Informatique) de la Universidad Paris-Sur).

Su resumen es

The most well-known feature of floating-point arithmetic is the limited precision, which creates round-off errors and inaccuracies. Another important issue is the limited range, which creates underflow and overflow, even if this topic is dismissed most of the time. This article shows a very simple example: the average of two floating-point numbers. As we want to take exceptional behaviors into account, we cannot use the naive formula (x+y)/2. Based on hints given by Sterbenz, we first write an accurate program and formally prove its properties. An interesting fact is that Sterbenz did not give this program, but only specified it. We prove this specification and include a new property: a precise certified error bound. We also present and formally prove a new algorithm that computes the correct rounding of the average of two floating-point numbers. It is more accurate than the previous one and is correct whatever the inputs.

El trabajo se presentará en el ICFEM 2015 (The 17th International Conference on Formal Engineering Methods).

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

Se ha publicado un artículo de razonamiento formalizado en Coq sobre geometría titulado A synthetic proof of Pappus’ theorem in Tarski’s geometry

Sus autores son Gabriel Braun y Julien Narboux (del Équipe Informatique Géométrique et Graphique en la Universidad de Estrasburgo, Francia).

Su resumen es

In this paper, we report on the formalization of a synthetic proof of Pappus’ theorem. We provide two versions of the theorem: the first one is proved in neutral geometry (without assuming the parallel postulate), the second (usual) version is proved in Euclidean geometry. The proof that we formalize is the one presented by Hilbert in The Foundations of Geometry which has been detailed by Schwabhäuser, Szmielew and Tarski in part I of Metamathematische Methoden in der Geometrie. We highlight the steps which are still missing in this later version. The proofs are checked formally using the Coq proof assistant. Our proofs are based on Tarski’s axiom system for geometry without any continuity axiom. This theorem is an important milestone toward obtaining the arithmetization of geometry which will allow us to provide a connection between analytic and synthetic geometry.

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