Fork me on GitHub
Math for the people, by the people.

User login

Resolution with Skolem functions

Primary tabs

Resolution with Skolem functions

Ok, I have another question (please forgive me).

I am not sure how to use resolution with clauses containing Skolem functions.

Say I am given the following clauses in conjugate normal form:
1) ~E(x) | V(x) P(f(x))
2a) E(f(x))
2b) G(f(x))
3) ~G(x) | ~V(x)
4) ~P(x) | ~G(x)

4) is the negated conclusion. Would the following derivation be correct?
Proof:
2b and 3 with {x/f(x)} entails 5): ~V(f(x))
1 and 2a with {x/f(x)} entails 6): V(f(x)) | P(f(f(x)))
5 and 6 entails 7): P(f(f(x)))
2b and 4 with {x/f(x)} entails 8): ~P(f(x))
4 and 8 with {f(x)/f(f(x))} entails an empty clause. End of proof.

Basically I do not really understand what is going on when we substitute with these Skolem functions, so I cannot see if what I am doing makes sense or not. Help please!


Subscribe to Comments for "Resolution with Skolem functions"