(Principiante) Probar argumentos con resolución con pasos detallados

Question

Soy muy nuevo en la resolución y me gustaría utilizarla para demostrar los dos argumentos siguientes. También me gustaría indicar las leyes de equivalencia utilizadas para obtener la forma normal de Skolem de las premisas y la conclusión negada:

---

1) $Premise ~ 1: ∃x ~ toad(x) \\ Premise ~ 2: ∀x ~ (toad(x) → slimy(x)) \\ Premise ~ 3: ∀x ~ (slimy(x) → muddy(x)) \\ Conclusion: ∃x ~ (muddy(x) ∧ toad(x))$

Intento:

Aparte de convertir la conclusión negada en la forma normal de la cláusula:

1. ∃x.(muddy(x) ∧ toad(x))        (Initial Conclusion)
2. ¬∃x.(muddy(x) ∧ toad(x))       (Negated Conclusion)
3. ∀x.¬(muddy(x) ∧ toad(x))       (DeMorgan Quantifer)
4. ∀x.(¬muddy(x) ∨ ¬toad(x))      (DeMorgan)
5. (¬muddy(x1) ∨ ¬toad(x1))       (∀-elim)

Además de convertir la premisa 1:

1. ∃x.toad(x)                     (Initial Premise 1)
2. toad(c)                        (Skolemization)

Aparte de convertir la premisa 2:

1. ∀x.(toad(x) → slimy(x))        (Initial Premise 2)
2. ∀x.(¬toad(x) ∨ slimy(x))       (Def. →)
3. (¬toad(x2) ∨ slimy(x2))        (∀-elim)

Aparte de convertir la premisa 3:

1. ∀x.(slimy(x) → muddy(x))       (Initial Premise 3)
2. ∀x.(¬slimy(x) ∨ muddy(x))      (Def. →)
3. (¬slimy(x3) ∨ muddy(x3))       (∀-elim)

Prueba de resolución real:

[ 1] {¬muddy(x1), ¬toad(x1)}   Negated Conclusion
[ 2] {toad(c)}                 Premise 1
[ 3] {¬toad(x2), slimy(x2)}    Premise 2
[ 4] {¬slimy(x3), muddy(x3)}   Premise 3
[ 5] {¬muddy(c)}               Res: 1, 2; θ = [x1/c]
[ 6] {¬slimy(x3), ¬toad(x3)}   Res: 1, 4; θ = [x1/x3]
[ 7] {slimy(c)}                Res: 2, 3; θ = [x2/c]
[ 8] {¬slimy(c)}               Res: 2, 6; θ = [x3/c]
[ 9] {}                        Res: 7, 8

---

2) $Premise 1: ∀x ~ (big(x) → (muddy(x) ∨ slimy(x))) \\ Premise 2: ∀x ~ ((slimy(x) ∧ ∃y ~ greater(x, y)) → gobbles(x, x)) \\ Premise 3: ∀x ~ ((big(x) ∧ muddy(x)) → ∃y ~ (toad(y) ∧ gobbles(x, y))) \\ Conclusion: ∀x ~ ((big(x) ∧ greater(x, shrek)) → ∃z ~ gobbles(x, z))$

Intento:

Aparte de convertir la conclusión negada en la forma normal de la cláusula:

1. ∀x.((big(x) ∧ greater(x,shrek)) → ∃z.gobbles(x,z))    (Initial Conclusion)
2. ¬∀x.((big(x) ∧ greater(x,shrek)) → ∃z.gobbles(x,z))   (Negation)
3. ∃x.¬((big(x) ∧ greater(x,shrek)) → ∃z.gobbles(x,z))   (DeMorgan)
4. ∃x.¬(¬(big(x) ∧ greater(x,shrek)) ∨ ∃z.gobbles(x,z))  (Def. →)
5. ∃x.(¬¬(big(x) ∧ greater(x,shrek)) ∧ ¬∃z.gobbles(x,z)) (DeMorgan)
6. ∃x.(big(x) ∧ greater(x,shrek) ∧ ∀z.¬gobbles(x,z))     (Double Neg., DeMorgan)
7. big(c) ∧ greater(c,shrek) ∧ ∀z.¬gobbles(c,z)          (Skolemization)

Además de convertir la premisa 1:

1. ∀x(big(x) → (muddy(x) ∨ slimy(x)))        (Initial Premise 1)
2. ∀x(¬big(x) ∨ (muddy(x) ∨ slimy(x)))       (Def. →)
3. ¬big(x2) ∨ (muddy(x2) ∨ slimy(x2))        (∀-elim)

Aparte de convertir la premisa 2:

1. ∀x.((slimy(x) ∧ ∃y.greater(x,y)) → gobbles(x,x))         (Initial Premise 2)
2. ∀x.(¬(slimy(x) ∧ ∃y.greater(x,y)) ∨ gobbles(x,x))        (Def. →)
3. ∀x.((¬slimy(x) ∧ ¬∃y.greater(x,y)) ∨ gobbles(x,x))       (DeMorgan)
4. ∀x.((¬slimy(x) ∧ ∀y.¬greater(x,y)) ∨ gobbles(x,x))       (DeMorgan)
5. ((¬slimy(x3) ∧ ¬greater(x3,y1)) ∨ gobbles(x3,x3))        (∀-elim)

Aparte de convertir la premisa 3:

1. ∀x.((big(x) ∧ muddy(x)) → ∃y.(toad(y) ∧ gobbles(x,y)))         (Initial Premise 3)
2. ∀x.(¬(big(x) ∧ muddy(x)) ∨ ∃y.(toad(y) ∧ gobbles(x,y)))        (Def. →)
3. ∀x.((¬big(x) ∨ ¬muddy(x)) ∨ ∃y.(toad(y) ∧ gobbles(x,y)))        (DeMorgan)
4. ∀x.((¬big(x) ∨ ¬muddy(x)) ∨ (toad(f(y)) ∧ gobbles(x,f(y))))     (Skolemization)
5. ((¬big(x4) ∨ ¬muddy(x4)) ∨ (toad(f(y)) ∧ gobbles(x4,f(y))))     (∀-elim)
6. ((¬big(x4) ∨ ¬muddy(x4)) ∨ toad(f(y))) ∧ ((¬big(x4) ∨ ¬muddy(x4)) ∨ gobbles(x4,f(y))) (Distribution)

Prueba de resolución real:

[ 1] {big(c)}                                             ∧-elim-1 Negated Conclusion, then ∧-elim-1 again 
[ 2] {greater(c,shrek)}                                   ∧-elim-1 Negated Conclusion, then ∧-elim-2 
[ 3] {¬gobbles(c,x1)}                                     ∧-elim-2 Negated Conclusion, ∀-elim
[ 4] {¬big(x2), muddy(x2), slimy(x2)}                     Premise 1
[ 5] {¬slimy(x3), ¬greater(x3,y1), gobbles(x3,x3)}        Premise 2
[ 6] {¬big(x4), ¬muddy(x4), toad(f(y))}                   Premise 3a ∧-elim-1
[ 7] {¬big(x4), ¬muddy(x4), gobbles(x4,f(y))}             Premise 3b ∧-elim-2                                     
How to proceed?

Answer 1

Para 1), la cláusula que se obtiene para $\exists x toad(x)$ debe ser $\{ toad(c) \}$ es decir, aquí hay que utilizar una constante, no una variable. Cuando se elimina un cuantificador existencial y se sustituye la variable cuantificada por ese cuantificador existencial por una constante, se llama Skolemización.

Esta constante debería utilizarse (sustituyendo las variables para unificar) también durante la resolución posterior, por ejemplo, en la línea 5 se obtendría $\{ \neg muddy(c) \}$ . De hecho, en la línea 7 se obtendría $\{ slimy(c) \}$ y en la línea 8 $\{ \neg slimy(c) $ , los cuales se resuelven en la cláusula vacía $\{ \}$ y ya está.

Para la 2), necesitas negar toda la conclusión, lo que te lleva a $\exists x (big(x) \land greater(x,shrek) \land \forall z \neg gobbles(x,z))$ y por Skolemización se obtiene así $big(c) \land greater(c,shrek) \land \forall z \neg gobbles(c,z)$ y, por tanto, las cláusulas $\{ big(c) \}$ , $\{ greater(c,shrek) \}$ y $\{ \neg gobbles(c,x1) \}$