RA2013: Razonamiento por casos y por inducción (1)

PorJosé A. Alonso

La clase de hoy del curso de Razonamiento automático ha tenido dos partes: comentar las soluciones de los ejercicios de la relación 4 y empezar el estudio del tema 4.

En la relación 4 se define la función cons que añade un elemento al final de la lista y se demuestra algunas de sus propiedades. Lo interesante es el uso de algunas propiedades en la demostración de otras (como en el ejercicio 5). Las ejercicios y sus soluciones son
Read More “RA2013: Razonamiento por casos y por inducción (1)”

Certified Kruskal’s tree theorem

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre órdenes titulado Certified Kruskal’s tree theorem.

Su autor es Christian Sternagel (del Japan Advanced Institute of Science and Technology).

Su resumen es

This paper gives the first formalization of Kruskal’s tree theorem in a proof assistant. More concretely, an Isabelle/HOL development of Nash-Williams’ minimal bad sequence argument for proving the tree theorem is presented. Along the way, the proofs of Dickson’s lemma and Higman’s lemma are discussed.

El trabajo se presentará en el CPP 2013 (3rd International Conference on Certified Programs and Proofs).

El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.

Proof Pearl: A probabilistic proof for the Girth-Chromatic number theorem

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle sobre
teoría de grafos titulado Proof Pearl: A probabilistic proof for the Girth-Chromatic number theorem.

Su autor es Lars Noschinski (de la Universidad Técnica de Munich, Alemania).

Su resumen es

The Girth-Chromatic number theorem is a theorem from graph theory, stating that graphs with arbitrarily large girth and chro- matic number exist. We formalize a probabilistic proof of this theorem in the Isabelle/HOL theorem prover, closely following a standard textbook proof and use this to explore the use of the probabilistic method in a theorem prover.

El trabajo se presentó en el ITP 2012 (Interactive Theorem Proving).

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

RA2013: Razonamiento estructurado sobre programas con Isabelle/HOL (2)

PorJosé A. Alonso

En la clase de hoy del curso de Razonamiento automático hemos continuado la presentación de cómo se puede demostrar detalladamente propiedades de programas funcionales con Isabelle/HOL.

Para ello, se visto cómo representar en Isabelle/HOL las demostraciones de propiedades de programas estudiadas en el tema 2a (que se corresponden con el capítulo 13 del libro de G. Hutton Programming in Haskell).

Las demostraciones estudiadas son las correspondientes a las páginas 38 a 50 del tema 2a. Los métodos de demostración utilizados son razonamiento ecuacional, inducción sobre los números naturales, inducción sobre listas e inducción sobre esquemas correspondientes a definiciones recursivas.

La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “RA2013: Razonamiento estructurado sobre programas con Isabelle/HOL (2)”

Reseña: A graph library for Isabelle

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle titulado A graph library for Isabelle.

Su autor es Lars Noschinski (de la Universidad Técnica de Munich, Alemania).

Su resumen es

In contrast to other areas of such as analysis, number theory or probability theory, no standard library for graph theory has yet evolved for the Isabelle/HOL proof assistant. We present a formalization of directed graphs and essential related concepts. The library supports general infinite directed graphs (digraphs) with labeled and parallel arcs, but care has been taken not to complicate reasoning on more restricted classes of digraphs.

We use this library to formalize a characterization of Euler Digraphs and a to verify a method of checking Kuratowski subgraphs used in the LEDA library.

El código de la teoría en Isabelle se encuentra aquí.