LI2011: Resolución en lógica de primer orden

PorJosé A. Alonso

En la clase de hoy del curso Lógica Informática se ha presentado la resolución en la lógica de primer orden como ampliación del presentado en el tema 5 para la lógica proposicional.

Las principales diferencias se encuentran en la unificación, separación de variables y factorización.

Además, se ha presentado el sistema Prover9 que busca automáticamente dem ostraciones por resolución.

Como tarea pendientes se propone la resolución de los ejercicios del tema 11 del libro de ejercicios.

Las transparencias de esta clase son las del tema 11
Read More “LI2011: Resolución en lógica de primer orden”

I1M2010: Búsqueda en escalada en Haskell

PorJosé A. Alonso

En la clase de hoy de Informática de 1º del Grado en Matemáticas hemos continuado el estudio de la resolución de problemas mediante búsqueda en espacios de estados, introduciendo el patrón de búsqueda en escalada y resolviendo con dicho patrón el problema del cambio de monedas y el algoritmo de Prim del árbol de expansión mínimo.

Las transparencias usadas en la clase son las páginas 44-55 del tema 23:
Read More “I1M2010: Búsqueda en escalada en Haskell”

I1M2010: Búsqueda por primero el mejor en Haskell

PorJosé A. Alonso

En la clase de hoy de Informática de 1º del Grado en Matemáticas hemos continuado el estudio de la resolución de problemas mediante búsqueda en espacios de estados.

La clase comenzó representando el problema del 8 puzzle en Haskell de acuerdo con el patrón de búsqueda en espacios de estados.

A continuación se comprobó la imposibilidad de resolver algunas instancias del problema con dicho patrón y cómo a partir de dicho patrón se puede obtener el de búsqueda por primero el mejor

Finalmente, se resolvió el problema del 8 puzzle mediante búsqueda por primero el mejor.

Las transparencias usadas en la clase son las páginas 38-43 del tema 23:
Read More “I1M2010: Búsqueda por primero el mejor en Haskell”

LI2011: Formas normales de Skolem

PorJosé A. Alonso

En la clase de hoy del curso Lógica Informática se estudiado cómo se puede diseñar un procedimiento de forma que dada una fórmula F obtenga otra sin cuantificadores G que sea equisatisfacible (es decir, que G es satisfacible precisamente si lo es F). Con dicho procedimiento se calcula la forma normal de Skolem.

Las transparencias de esta clase son las páginas 1 a 14 del tema 9
Read More “LI2011: Formas normales de Skolem”