Reseña: A formal proof of Kruskal’s tree theorem in Isabelle/HOL

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado A formal proof of Kruskal’s tree theorem in Isabelle/HOL.

Su autor es Christian Sternagel (del JAIST, Japón).

Su resumen es

We give the first formalization of Kruskal’s tree theorem in a proof assistant – the closure of a long-standing challenge. More concretely, we present our Isabelle/HOL development of Nash-Williams’ minimal bad sequence argument for proving the tree theorem. Along the way, we discuss proofs of Dickson’s lemma and Higman’s lemma; and close all gaps in the original proofs.

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

I1M2012: El TAD (tipo abstracto de datos) de las tablas en Haskell

PorJosé A. Alonso

En la clase de hoy de Informática de 1º del Grado en Matemáticas se ha estudiado el TAD (tipo abstracto de datos) de las tablas y tres implementaciones en Haskell: como funciones, como listas de asociación y como matrices.

Una tabla (array en inglés y tableau en francés) es una colección de elementos (valores) a los que se accede mediante sus índices.

El contenido de la clase ha sido el siguiente:

  • la signatura del TAD de las tablas;
  • las propiedades del TAD de las tablas;
  • las implementaciones, en Haskell, de las tablas mediante funciones, listas de asociación y matrices y
  • la comprobación con QuickCheck de sus propiedades.

Read More “I1M2012: El TAD (tipo abstracto de datos) de las tablas en Haskell”

LMF2013: Tableros semánticos

PorJosé A. Alonso

En la clase de hoy del curso Lógica matemática y fundamentos se ha presentado un nuevo sistema deductivo: los tableros semánticos.

Hemos visto cómo los problemas de tautología y de consecuencia lógica se reducen a problemas de consistencia:

  • F es una tautología syss \{\neg F\} es inconsistente.
  • F es consecuencia lógica de S syss S \cup \{\neg F\} es inconsistente.

Por tanto, para resolver ambos problemas basta con tener un procedimiento sistemático de búsqueda de modelos. Uno de dichos procedimientos es el de tableros semánticos.

Una ventaja de los tableros semánticos frente a la deducción natural es la reducción del número lo que facilita su automatización.

Además, se ha presentado el sistema Tree Proof Generator que busca automáticamente el tablero semántico correspondiente a la fórmula introducida.

Las transparencias de esta clase son las del tema 3 (tableros proposicionales) y las del tema 9 (tableros de primer orden)
Read More “LMF2013: Tableros semánticos”

Reseña: Formalizing Knuth-Bendix orders and Knuth-Bendix completion

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre sistemas de reescritura titulado Formalizing Knuth-Bendix orders and Knuth-Bendix completion.

Sus autores son Christian Sternagel (del Instituto japonés de ciencias y tecnología) y René Thiemann (de la Univ. de Innsbruck, Austria).

El trabajo se presentará en junio en la RTA 2013 (24th International Conference
on Rewriting Techniques and Applications).

Su resumen es

We present extensions of our Isabelle Formalization of Rewriting that cover two historically related concepts: the Knuth-Bendix order and the Knuth-Bendix completion procedure. The former, besides being the first development of its kind in a proof assistant, is based on a generalized version of the Knuth-Bendix order. We compare our version to variants from the literature and show all properties required to certify termination proofs of TRSs. The latter comprises the formalization of important facts that are related to completion, like Birkhoff’s theorem, the critical pair theorem, and a soundness proof of completion, showing that the strict encompassment condition is superfluous for finite runs. As a result, we are able to certify completion proofs.

El código con las correspondientes teorías Isabelle se encuentra en la versión 2.10 de IsaFoR/CeTA.