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

En la 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 “RA2013: Verificación de propiedades de recorridos en árboles binarios con Isabelle/HOL”

LI2013-14: La lógica de Prolog

En la clase de hoy del curso Lógica Informática se ha realizado una introducción a la programación lógica con Prolog como aplicación de la resolución en la lógica de primer orden.

Se ha presentado el sistema deductivo de Prolog en tres fases: proposicional, relacional y funcional. En cada una se ha comentado cómo representar el conocimiento, cómo realizar consultas y cómo es el razonamiento de Prolog para calcular las respuestas.

En los siguiente vídeos se presenta el uso de Prolog y uso de SldRaw.

La clase se basa en los apuntes de Introducción a la programación lógica con Prolog.

Las transparencias de esta clase son las página 1 a 18 del tema 12
Read More “LI2013-14: La lógica de Prolog”

I1M2013: Evaluación perezosa en Haskell

En la clase de hoy de Informática de 1º del Grado en Matemáticas se ha estudiado la evaluación perezosa en Haskell. Se han visto la estrategias de evaluación perezosa e impaciente, se han comparado respecto de la terminación y el número de pasos necesarios en las computaciones, se ha aplicado a la computación con estructuras infinitas y se han visto casos en los que se aumenta la eficiencia con evaluación estricta.

Como ejemplo, se ha estudiado el cálculo de los números primos mediante la criba de Erastótenes.

Las transparencias usadas en la clase son las del tema 10

El problema del granjero, la oveja y la col en Haskell

Recientemente, Justin Le ha publicado el artículo Wolf, goat, cabbage: The list MonadPlus & logic problems en el que explica cómo se pueden usar las mónadas para resolver el problema del granjero, el lobo, la oveja y la col. El enunciado de dicho problema es el siguiente

Un granjero fue al mercado y compró un lobo, una oveja y una col. Para volver a su casa tenía que cruzar un río. El granjero dispone de una barca para cruzar a la otra orilla, pero en la barca solo caben él y una de sus compras. Además, si el lobo se queda solo con la cabra se la come y si la cabra se queda sola con la col se la come.

El reto del granjero era cruzar él mismo y dejar sus compras a la otra orilla del río, dejando cada compra intacta. ¿Cómo lo hizo?

A partir del artículo, he elaborado la siguiente relación de ejercicios (para la asignatura de Informática de 1º del Grado en Matemáticas y para la siguiente versión del libro Piensa en Haskell). En ella se incluyen soluciones sin usar mónadas y con mónadas (concretamente, los ejercicios 12, 15 y 17).

La relación de ejercicios y sus soluciones es la siguiente
Read More “El problema del granjero, la oveja y la col en Haskell”

Fallos informáticos y verificación de programas

Una de las principales aplicaciones del razonamiento automático consiste en la verificación de programas. Por ello, en el comienzo de los cursos de razonamiento automático se suele comentar algunos de los fallos informáticos más famosos.

Una referencia básica sobre fallos informáticos es el libro de Ivars Peterson Error fatal: a la caza de fallos informáticos (publicado por Alianza Editorial en 1999) en el que se comenta algunos errores de programación que tuvieron funestas consecuencias y presenta a alguna de las personas que se dedican a «cazar» estos fallos antes de que provoquen desgracias irreparables.

Otras recopilaciones más recientes de fallos informáticos son las siguientes: