LI2012: Ejercicios de formalización y demostración

En la clase de hoy, y la anterior, del curso Lógica Informática se han resuelto ejercicios de argumentación siguiento los siguientes pasos

  1. formalizar el argumento en lógica de primer orden,
  2. decidir mediante resolución y tablero semántico si el argumento es correcto,
  3. en el caso de que no sea correcto, extraer un contramodelo,
  4. en el caso de que sea correcto, demostrarlo por deducción natural.

Los ejercicios estudiados han sido

  1. En una pecera nadan una serie de peces. Se observa que: Hay algún pez x que para cualquier pez y, si el pez x no se come al pez y entonces existe un pez z tal que z es un tiburón o bien z protege al pez y. No hay ningún pez que se coma a todos los demás. Ningún pez protege a ningún otro. Por tanto, existe algún tiburón en la pecera.
  2. Algunas personas admiran a los que tienen bigote. Algunas personas no simpatizan con nadie que admire a los que tienen bigote. Luego algunas personas no son simpáticas a todos.
  3. Todo deprimido que estima a un submarinista es listo. Cualquiera que se estime a sí mismo es listo. Ningún deprimido se estima a sí mismo. Por tanto, ningún deprimido estima a un submarinista.
  4. Todos los robots obedecen a los amigos del programador jefe. Alvaro es amigo del programador jefe, pero Benito no le obedece. Por tanto, Benito no es un robot.

LI2012: Introducción a la programación lógica

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. lógica proposicional.

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.

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 páginas 1 a 18 del tema 13
Read More “LI2012: Introducción a la programación lógica”

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

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

LI2012: Modelos de Herbrand

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 del tema 11.