I am trying to prove using the resolution technique that the following two clauses are contradicting:
- $\forall_x Shaves(Barber, x) \iff \neg Shaves(x, x)$
- $\exists_x Shaves(x, Barber)$
After turing those into the conjunctive normal form and skolemization I get the following clauses:
- $\neg Shaves(Barber, x)\ \lor\ \neg Shaves(x, x)$
- $Shaves(Barber, x)\ \lor\ Shaves(x, x)$
- $Shaves(Someone, Barber)$
where $Someone$ is a Skolem constant (a Skolem function of of zero arity).
I am unable to prove that this set of clauses is contradicting. It looks like something is missing. Shouldn't there be a clause, which prevents $Someone$ from being a barber as well?