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)