Menu Close

Etiqueta: LI2013

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

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

LI2013: Ejercicio de deducción en lógica de primer orden

En la clase de hoy del curso Lógica Informática se han comentado las soluciones de ejercicios de deducción en lógica de primer orden mediante los 3 métodos (deducción natural, tableros semánticos y resolució). Concretamente, los ejercicios comentados son desde el 5.1 al 5.9 del capítulo 8 del libro de ejercicios:

  1. ∀x [P(x) → Q(x)] ͱ ∀xP(x) → ∀xQ(x)
  2. ∃x ¬P(x) ͱ ¬∀xP(x)
  3. ∀xP(x) ͱ ∀yP(y)
  4. ∀x [P(x) → Q(x)] ͱ ∀x ¬Q(x) → ∀x ¬P(x)
  5. ∀x [P(x) → ¬Q(x)] ͱ ¬∃x [P(x) ∧ Q(x)]
  6. ∀x ∀yP(x,y) ͱ ∀u ∀vP(u,v)
  7. ∃x ∃yP(x,y) ͱ ∃u ∃vP(u,v)
  8. ∃x ∀yP(x,y) ͱ ∀y ∃xP(x,y)
  9. ∃x [P(a) → Q(x)] ͱ P(a) → ∃xQ(x)

LI2013 Resolución en lógica de primer orden

En la primera parte de 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 G que no tenga cuantificadores, que esté en forma normal conjuntiva y que sea equisatisfacible con F (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.

En la segunda parte 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.

Como tarea pendientes se propone la resolución de los ejercicios de los temas 10 y 12 del libro de ejercicios.

Las transparencias de la primera parte son las del tema 10

LI2013: Tableros semánticos de primer orden y equivalencias lógicas

En la primera parte de la clase de hoy del curso Lógica Informática se ha presentado un nuevo sistema deductivo: los tableros semánticos de primer orden como ampliación del presentado en el tema 3 para la lógica proposicional.

En la segunda parte, se ha demostrado por deducción natural las principales equivalencias en lógica de primer orden. Además, se ha mostrado cómo hacer las demostraciones en Pandora como se muestra en este vídeo.

Las transparencias de esta clase son las finales del tema 8 y las del tema 9 que se muestran a continuación

LI2013: Deducción natural en lógica de primer orden (2)

En la clase de hoy del curso Lógica Informática se ha continuado el estudio de la deducción natural en lógica de primer orden. Se han comentado distintas equivalencias lógicas y se han demostrado por deducción natural y mediante tableros semánticos las siguientes equivalencias:

  • ¬∀xP(x) ≡ ∃x¬P(x)
  • ∀x(P(x) ∧ Q(x)) ≡ ∀xP(x) ∧ ∀xQ(x)

Las transparencias de esta clase son las páginas 14 a 20 del tema 8 que se muestran a continuación