Reseña: “Ordinals in HOL: Transfinite arithmetic up to (and beyond) ω₁”

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en HOL4 sobre teoría de conjuntos titulado Ordinals in HOL: Transfinite arithmetic up to (and beyond) ω₁.

Sus autores son Michael Norrish (del (Canberra Research Lab., NICTA) y Brian Huffman (de Galois, Inc.).

El trabajo se ha presentado esta semana en el ITP 2013 (4th Conference on
Interactive Theorem Proving).

Su resumen es

We describe a comprehensive HOL mechanisation of the theory of ordinal numbers, focusing on the basic arithmetic operations. Mechanised results include the existence of fixpoints such as ε₀ , the existence of normalforms, and the validation of algorithms used in the ACL2 theorem-proving system.

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

Reseña: Program verification based on Kleene algebra in Isabelle/HOL

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado Program verification based on Kleene algebra in Isabelle/HOL.

Sus autores son Alasdair Armstrong, Georg Struth y Tjark Weber (los dos primeros de la Universidad de Sheffield y el tercero de la de Uppsala).

El trabajo se ha presentado esta semana en el ITP 2013 (4th Conference on
Interactive Theorem Proving).

Su resumen es

Schematic Kleene algebra with tests (SKAT) supports the equational verification of flowchart scheme equivalence and captures simple while programs with assignment statements. We formalise SKAT in Isabelle/HOL, using the quotient type package to reason equationally in this algebra. We apply this formalisation to a complex flowchart transformation proof from the literature. We extend SKAT with assertion statements and derive the inference rules of Hoare logic. We apply this extension in simple program verification examples and the derivation of additional Hoare-style rules. This shows that algebra can provide an abstract semantic layer from which different program analysis and verification tasks can be implemented in a simple lightweight way.

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

Reseña: Reading an algebra textbook (by translating it to a formal document in the Isabelle/Isar language)

PorJosé A. Alonso

Se ha publicado un artículo sobre formalización en Isabelle/Isar titulado Reading an algebra textbook.

Su autor es Clemens Ballarin (de la Technische Universität München) y lo presentó en el CICM 2013 (Conferences on Intelligent Computer Mathematics).

Su resumen es

We report on a formalisation experiment where excerpts from an algebra textbook are compared to their translation into formal texts of the Isabelle/Isar prover, and where an attempt is made in the formal text to stick as closely as possible with the structure of the informal counterpart. The purpose of the exercise is to gain understanding on how adequately a modern algebra text can be represented using the module facilities of Isabelle. Our initial results are promising.

Reseña: Inteligencia artificial avanzada

PorJosé A. Alonso

En la colección de textos de la UOC (Universitat Oberta de Catalunya) se ha publicado el libro Inteligencia artificial avanzada.

Sus autores son Raúl Benítez, Gerard Escudero y Samir Kanaan.

El libro está organizado de la forma siguiente: los métodos de búsqueda y optimización se describen en el apartado 2, donde se detallarán las técnicas de extracción de información de bases de datos que contengan información semántica, como por ejemplo web de noticias o las conversaciones entre diversos miembros de una red social.

Las técnicas de caracterización de datos se estudiarán en el apartado 3, describiendo las técnicas principales basadas en descomposición de los datos en modos principales. En el apartado 3 también se estudiarán las técnicas de extracción de características y un método de visualización de datos multidimensionales.

Los algoritmos de clasificación de datos se presentan en el apartado 4, en el que se estudiarán los principales métodos de clasificación y reconocimiento de patrones.

En el apartado 5 se explican algunas técnicas avanzadas de inteligencia evolutiva, algoritmos que utilizan reglas heurísticas inspiradas en el funcionamiento evolutivo de los sistemas biológicos.

El código del texto está escrito en Python. Una introducción a Python se encuentra en otro texto de la UOC: El lenguaje Python escrito por David Masip Rodó– El objetivo del texto es ayudar a comprender los ejemplos que se exponen en el libro de inteligencia artificial.

Ambos libros son la base de la asignatura Intel·ligència artificial avançada impartida por David Masip Rodó en el Màster en Enginyeria Informàtica de la UOC.

Reseña: El uso de los demostradores automáticos de teoremas para la enseñanza de la programación

PorJosé A. Alonso

Se ha publicado un artículo sobre el uso de Krakatoa en la enseñanza titulado El uso de los demostradores automáticos de teoremas para la enseñanza de la programación.

Su autora es Ana Romero (de la Universidad de la Rioja) y lo ha presentado en la Jenui 2013 (XIX Jornadas sobre la Enseñanza Universitaria de la Informática).

Su resumen es

La verificación formal de algoritmos, impartida en los estudios de Ingeniería Informática como parte de las asignaturas de programación, se suele explicar de manera “teórica” introduciendo los axiomas de la lógica de Hoare y realizando diversos ejercicios de verificación (a mano) de pequeños programas. Aunque los alumnos han debido adquirir previamente los conocimientos de Lógica necesarios, muchos de ellos presentan serias dificultades para expresar formalmente los distintos pasos de las pruebas de corrección planteadas. En esta experiencia se ha decidido utilizar como herramienta de apoyo para explicar la verificación formal de algoritmos un demostrador automático de teoremas llamado Krakatoa. Esta herramienta permitirá a los estudiantes visualizar de manera interactiva los distintos pasos necesarios para probar la corrección de un programa, reflexionar sobre los razonamientos seguidos y comprender la importancia de la verificación de algoritmos para mejorar la fiabilidad de nuestros programas.