RA2014: Deducción natural con Isabelle/HOL

PorJosé A. Alonso

En la segunda parte de la clase de hoy del curso de Razonamiento automático se ha presentado la deducción naturalcon Isabelle/HOL. La presentación se basa en los ejemplos del tema 2 y del tema 8 del curso de Lógica informática que, a su vez, se basa en el capítulo 2 del libro de Huth y Ryan Logic in Computer Science (Modelling and reasoning about systems).

La página al lado de cada ejemplo indica la página de las transparencias donde se encuentra la demostración.

Para cada ejemplo se presentan distintas demostraciones. La primera intenta reflejar la demostración de las transparencias, las siguientes van eliminando detalles de la prueba hasta la última que es automática.

A los largos de los ejemplos se van comentando los elementos del lenguaje conforme van entrando en el juego.

La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “RA2014: Deducción natural con Isabelle/HOL”

Reseña: Budget imbalance criteria for auctions: A formalized theorem

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre economía titulado Budget imbalance criteria for auctions: A formalized theorem.

Sus autores son Marco B. Caminati, Manfred Kerber y Colin Rowat (de la Univ. de Birmingham).

Su resumen es

We present an original theorem in auction theory: it specifies general conditions under which the sum of the payments of all bidders is necessarily not identically zero, and more generally not constant. Moreover, it explicitly supplies a construction for a finite minimal set of possible bids on which such a sum is not constant. In particular, this theorem applies to the important case of a second-price Vickrey auction, where it reduces to a basic result of which a novel proof is given. To enhance the confidence in this new theorem, it has been formalized in Isabelle/HOL: the main results and definitions of the formal proof are re- produced here in common mathematical language, and are accompanied by an informal discussion about the underlying ideas.

El trabajo se ha presentado en la 6th Podlasie Conference on Mathematics 2014.

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

RA2014: Verificación de propiedades de recorridos en árboles binarios con Isabelle/HOL

PorJosé A. Alonso

En primera parte de la clase de hoy del curso de Razonamiento automático se han comentado las soluciones de los ejercicios de la relación 7. En dicha relación se definen funciones para recorrer árboles binarios y se demuestran con Isabelle/HOL algunas de sus propiedades.

Los ejercicios y sus soluciones se muestran a continuación
Read More “RA2014: Verificación de propiedades de recorridos en árboles binarios con Isabelle/HOL”