I am very new to resolution and would like to use it to prove the following two arguments. I also would like to indicate the laws of equivalence used to obtain Skolem Normal Form of the premises and the negated conclusion:
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))$
Attempt:
Aside for turning negated conclusion into clausal normal form:
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)
Aside for converting Premise 1:
1. ∃x.toad(x) (Initial Premise 1)
2. toad(c) (Skolemization)
Aside for converting Premise 2:
1. ∀x.(toad(x) → slimy(x)) (Initial Premise 2)
2. ∀x.(¬toad(x) ∨ slimy(x)) (Def. →)
3. (¬toad(x2) ∨ slimy(x2)) (∀-elim)
Aside for converting Premise 3:
1. ∀x.(slimy(x) → muddy(x)) (Initial Premise 3)
2. ∀x.(¬slimy(x) ∨ muddy(x)) (Def. →)
3. (¬slimy(x3) ∨ muddy(x3)) (∀-elim)
Actual Resolution Proof:
[ 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))$
Attempt:
Aside for turning negated conclusion into clausal normal form:
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)
Aside for converting Premise 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)
Aside for converting Premise 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)
Aside for converting Premise 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)
Actual Resolution Proof:
[ 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?
For 1), the clause you get for $\exists x toad(x)$ should be $\{ toad(c) \}$, i.e. you need to use a constant here, not a variable. When you remove an existential quantifier and substitute a constant for the variable that was quantified by that existential quantifier, it is called Skolemization.
This constant should then be used (substituted for variables in order to unify) during subsequent resolution as well, e.g. on line 5 you would get $\{ \neg muddy(c) \}$. In fact, on line 7 you would get $\{ slimy(c) \}$, and on line 8 $\{ \neg slimy(c) $, the two of which resolve to the empty clause $\{ \}$, and you are done.
For 2), you need to negate the whole conclusion, which gets you $\exists x (big(x) \land greater(x,shrek) \land \forall z \neg gobbles(x,z))$, and by Skolemization you thus get $big(c) \land greater(c,shrek) \land \forall z \neg gobbles(c,z)$, and thus clauses $\{ big(c) \}$, $\{ greater(c,shrek) \}$, and $\{ \neg gobbles(c,x1) \}$