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!

- Forums
- Planetary Bugs
- HS/Secondary
- University/Tertiary
- Graduate/Advanced
- Industry/Practice
- Research Topics
- LaTeX help
- Math Comptetitions
- Math History
- Math Humor
- PlanetMath Comments
- PlanetMath System Updates and News
- PlanetMath help
- PlanetMath.ORG
- Strategic Communications Development
- The Math Pub
- Testing messages (ignore)

- Other useful stuff
- Corrections