Coq

Se ha publicado un artículo de razonamiento formalizado en Coq sobre grafos titulado Depth-first search and strong connectivity in Coq.

Su autor es François Pottier (del grupo Gallium en el INRIA de Rocquencourt).

Su resumen es

Using Coq, we mechanize Wegener’s proof of Kosaraju’s linear-time algorithm for computing the strongly connected components of a directed graph. Furthermore, also in Coq, we define an executable and terminating depth-first search algorithm.

El trabajo se ha presentado en las Journées Francophones des Langages Applicatifs (JFLA 2015).

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 Automated generation of machine verifiable and readable proofs: A case study of Tarski’s geometry.

Sus autores son

• Sana Stojanovic Durdevic (de la Univ. de Belgrado, Serbia).
• Julien Narboux (de la Univ. de Estrasburgo) y
• Predrag Janicic (del Automated Reasoning GrOup (ARGO) en la Univ. de Belgrado, Serbia)

Su resumen es

The power of state-of-the-art automated and interactive the-orem provers has reached the level at which a significant portion of non-trivial mathematical contents can be formalized almost fully automat-ically. In this paper we present our framework for the formalization of mathematical knowledge that can produce machine verifiable proofs (for different proof assistants) but also human-readable (nearly textbook-like) proofs. As a case study, we focus on one of the twentieth century classics – a book on Tarski’s geometry. We tried to automatically generate such proofs for the theorems from this book using resolution theorem provers and a coherent logic theorem prover. In the first experiment, we used only theorems from the book, in the second we used additional lemmas from the existing Coq formalization of the book, and in the third we used specific dependency lists from the Coq formalization for each theorem. The results show that 37% of the theorems from the book can be auto-matically proven (with readable and machine verifiable proofs generated) without any guidance, and with additional lemmas this percentage rises to 42%. These results give hope that the described framework and other forms of automation can significantly aid mathematicians in developing formal and informal mathematical knowledge.

El trabajo se ha publicado en Annals of Mathematics and Artificial Intelligence.

Se ha publicado un artículo de razonamiento formalizado en Coq titulado Fibonacci numbers and the Stern-Brocot tree in Coq.

Sus autor es José Grimm (del Marelle Team en el Inria, Sophia-Antipolis Méditerranée).

Su resumen es

In this paper, we study the representation of a number by some other numbers. For instance, an integer may be represented uniquely as a sum of powers of two; if each power of two is allowed to appear at most twice, the number of representations is s(n), a sequence studied by Dijkstra, that has many nice properties proved here with the use of the proof assistant Coq. It happens that every rational number x is uniquely the quotient s(n)/s(n+1) as noticed by Stern, and that the integer n is related to the continued fraction expansion of x. It happens that by reverting the bits on n, one gets a sequence of rational numbers with increasing denominators that goes from 1 to x and becomes nearer at each iteration; this was studied by Brocot, whence the name Stern-Brocot tree. An integer can also be represented as a sum of Fibonacci numbers; we study R(n) the number of such representations; there is uniqueness for the predecessors of Fibonacci numbers; there is also uniqueness under additional constraints (for instance, no two consecutive Fibonacci numbers can be used, or no two consecutive numbers can be omitted).

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