LI2013

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)

En la clase de hoy del curso Lógica Informática de han comentado las soluciones de ejercicios de resolución en lógica de primer orden. Concretamente, desde el ejercicio 13 al 14.5 del capítulo 12 del libro de ejercicios.

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