FNS de examen 2026

 

Para aplicar resolución usamos las premisas + negación de la conclusión.

Premisa 1: ∀x[G(x) → ∃yP(y)]

∀x[¬G(x) ∨ ∃yP(y)]

∀x[¬G(x) ∨ P(f(x))]

Cláusula: ¬G(x) ∨ P(f(x))

 

Premisa 2: ∀x∀y[P(y) → ¬T(x,y)]

∀x∀y[¬P(y) ∨ ¬T(x,y)]

Cláusula: ¬P(y) ∨ ¬T(x,y)

 

Premisa 3: ∀x∃yT(y,x)

∀xT(g(x),x)

Cláusula: T(g(x),x)

 

Negación de la conclusión:

¬∀x¬G(x)

∃xG(x)

G(a)

 

Conjunto de cláusulas: { ¬G(x) ∨ P(f(x)), ¬P(y) ∨ ¬T(x,y), T(g(x),x), G(a) }

​