LI2013: Razonamiento en Prolog sobre listas

En la clase de hoy del curso Lógica Informática se ha estudiado cómo se representan las listas en Prolog, cómo se diseñan programas sobre listas y cómo Prolog obtiene las respuestas.

Para la construcción de los árboles de deducción de Prolog se ha utilizado el programa SldDraw. El uso del programa se muestra en el siguiente vídeo.

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 18 a 27 del tema 12
Read More “LI2013: Razonamiento en Prolog sobre listas”

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