LI2011-12

La clase de hoy del curso Lógica Informática ha consistido en la resolución de ejercicios de la lógica de primer orden. Los ejercicios corresponden al capítulo 11 del libro de ejercicios.

Los ejercicios resueltos son los siguientes:

• 13.1 y 13.3: Decidir si dos términos son unificables, y en su caso calcular un unificador de máxima generalidad.
• 14.1: Demostrar la validez de una fórmula por resolución, tableros semánticos y deducción natural.
• 14.2: Decidir por resolución la validez de una fórmula.
• 29: Dado un programa lógico y una pregunta, calcular las respuestas.
• 23: Formalizar un argumento y decidir su validez.

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 y como base para programar los conceptos de la lógica proposicional.

En primer lugar, 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 segundo lugar, se ha estudiado el procesamiento de listas en Prolog. Se destaca la analogía con el de los números naturales.

En tercer lugar, hemos vistos cómo se puede representar el conocimiento y las consultas “casi en lenguaje natural” usando operadores.

En cuarto lugar, hemos estudiado cómo se puede mejorar la búsqueda usando cortes.

Finalmente, se ha visto cómo definir la negación como fallo y cómo razonar con conocimiento negativo.

Los apuntes de esta clase son Introducción a la programación lógica con Prolog (páginas 1-26).

Las transparencias de esta clase son las del tema 12
Read More “LI2011-12: Introducción a la programación lógica con Prolog”

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 demostraciones 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-12: Resolución en lógica de primer orden”

En la clase de hoy del curso Lógica Informática se estudiado cómo se puede puede reducir la consistencia de conjuntos de cláusulas de primer orden a la consistencia de conjuntos de cláusulas proposicionales.

En primer lugar, se ha observado que la reducción es inmediata en el caso de fórmulas sin variables.

A continuación se han presentado procedimientos para construir los universos de Herbrand, las bases de Herbrand y las interpretaciones de Herbrand. Así como un procedimiento que transforma modelos de conjuntos de cláusulas en modelos de Herbrand. Por tanto, la consistencia de un conjunto de cláusulas se reduce a la búsqueda de modelos de Herbrand.

Finalmente, se ha explicado el teorema de Herbrand y su aplicación para decidir la consistencia de un conjunto de cláusulas buscando un subconjunto finito de su extensión de Herbrand que sea consistente (en el sentido proposicional).

Las transparencias de la clase son las tema 10.

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. A partir de las formas se Skolem se obtienen las formas clausales.

Las transparencias de esta clase son las del tema 9
Read More “LI2011-12: Formas normales de Skolem y cláusulas”