Steps towards verified implementations of HOL Light

PorJosé A. Alonso

Una de la líneas de trabajo dentro de la automatización del razonamiento es la verificación de sistemas de razonamiento. En dicha línea se ha publicado un trabajo titulado Steps towards verified implementations of HOL Light.

Sus autores son

Su resumen es

This short paper describes our plans and progress towards construction of verified ML implementations of HOL Light: the first formally proved soundness result for an LCF-style prover. Building on Harrison’s formalisation of the HOL Light logic and our previous work on proof-producing synthesis of ML, we have produced verified implementations of each of HOL Light’s kernel functions. What remains is extending Harrison’s soundness proof and proving that ML’s module system provides the required abstraction for soundness of the kernel to relate to the entire theorem prover. The proofs described in this paper involve the HOL Light and HOL4 theorem provers and the OpenTheory toolchain.

El trabajo se presentó en el ITP 2013 (4th Conference on Interactive Theorem Proving).

Introducción a la demostración asistida por ordenador con Isabelle/HOL

PorJosé A. Alonso

En el libro Introducción a la demostración asistida por ordenador con Isabelle/HOL he recopilado los temas y relaciones de ejercicios del curso de Razonamiento automático (2012-13).

El curso es una introducción a la demostración asistida por ordenador con Isabelle/HOL y consta de tres niveles.

En el primer nivel se presenta la formalización de las demostraciones por deducción natural. La presentación se basa en la realizada en los cursos de Lógica informática (de 2º del Grado en Informática) y Lógica matemática y fundamentos (de 3º del Grado en Matemáticas), en concreto en los temas de deducción natural proposicional y de primer orden. En este nivel se incluye los 3 primeros temas y las 6 primeras relaciones de ejercicios.

En el segundo nivel se presenta la programación funcional en Isabelle/HOL y el razonamiento sobre programas. La presentación se basa en la introducción a la programación con Haskell realizada en los cursos de Informática (de 1º del Grado en Matemáticas) y Programación declarativa (de 3º del Grado en Informática), en concreto en el tema 8 (para el razonamiento sobre programas) y en los restantes 9 primeros temas (para la programación funcional). En este nivel se incluye los temas 4, 5 y 6 y las relaciones de ejercicios desde la 7 a la 21.

En el tercer nivel se presentan casos de estudios y extensiones de la lógica para trabajar con conjuntos, relaciones y funciones. En este nivel se incluyen los temas 7 y 8 y las relaciones de ejercicios 22 y 23.

Tanto los temas como las relaciones de ejercicios se presentan como teorías de Isabelle/HOL (versión Isabelle2013). Conforme se necesitan se va comentando los elementos del Isabelle/HOL.

De Isabelle2013 se dispone se dispone de versiones libres para Linux, Windows y Mac OS X. Para instalarlo basta seguir la guía de instalación.

Los números de Ulam en Haskell

PorJosé A. Alonso

Los números de Ulam son los elementos de la sucesión u(n) definida por u(1) = 1, u(2) = 2 y, para n > 2, u(n) es el entero más pequeño que se puede escribir exactamente de una forma como suma de dos términos anteriores diferentes entre sí.

Según la definición, 3=1+2 es un número de Ulam y 4=1+3 también es un número de Ulam (la suma 4=2+2 no cuenta porque los términos previos deben ser distintos). El entero 5 no es un número de Ulam porque 5=1+4=2+3.

Los primeros términos de la sucUlam son: 1, 2, 3, 4, 6, 8, 11, 13, 16, 18, 26, 28, 36, 38, 47, 48, 53, 57, 62, 69, 72, 77, 82, 87, 97, 99.

Esta sucesión fue definida por el matemático polaco Stanislaw Ulam y
publicada en SIAM Review en 1964.

A partir de los artículos de la Wikipedia y de MathWorld sobre los números de Ulam elaborado la siguiente relación de ejercicios de Haskell para la asignatura de Informática de 1º del Grado en Matemáticas.

En la relación se presentan cuatro definiciones de los números de Ulam, se compara su eficiencia, se muestra algunas de sus propiedades terminando con los números de Ulam generalizados.
Read More “Los números de Ulam en Haskell”

Generic datatypes à la carte

PorJosé A. Alonso

Se ha publicado un artículo de automatización del razonamiento en Coq titulado Generic datatypes à la carte.

Sus autores son Steven Keuchel y Tom Schrijvers (de la Universidad de Gante, Bélgica).

Su resumen es

Formal reasoning in proof assistants, also known as mechanization, has high development costs. Building modular reusable components is a key issue in reducing these costs. A stumbling block for reuse is that inductive definitions and proofs are closed to extension. This is a manifestation of the expression problem that has been addressed by the Meta-Theory à la Carte (MTC) framework in the context of programming language meta-theory. However, MTC’s use of extensible Church-encodings is unsatisfactory.

This paper takes a better approach to the problem with datatype- generic programming (DGP). It applies well-known DGP techniques to represent modular datatypes, to build functions from functor algebras with folds and to compose proofs from proof algebras by means of induction. Moreover, for certain functionality and proofs our approach can achieve more reuse than MTC: instead of composing modular components we provide a single generic definition once and for all.

El correspondiente código en Coq se encuentra aquí.

El trabajo se presentará en el WGP 2013 (9th ACM SIGPLAN Workshop on Generic Programming).

La Lógica en las ciencias computacionales

PorJosé A. Alonso

Se ha publicado un artículo sobre la enseñanza de la lógica titulado La Lógica en las ciencias computacionales.

Su autor es Edgar Serna M. (del Instituto Tecnológico Metropolitano, Medellín (Colombia)).

Su resumen es

En este trabajo se hace un análisis a la necesidad de incluir a la lógica en los procesos formativos en Ciencias Computacionales (CS por sus siglas en inglés). Se parte de un recorrido sobre la historia de la lógica en estas ciencias, posteriormente se describe la relación y la necesidad de incluirla en los procesos formativos relacionados, y al final se analiza qué, cuándo y qué tan profundo se debería trabajar en la formación en CS. Se trata de una revisión al estado del tema y a la importancia de incluirlo en los pregrados y en los posgrados en áreas de ciencias computacionales y tecnologías de información.

El artículo se ha publicado en la Revista Educación en Ingeniería.