Resolution of Barber paradox

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?

No, you don't need to specially add any such clause.

Here's where I think you might have gone wrong. The result is not 3 clauses (3 conjunctions). The result is a bunch of clauses. We get one clause of the form $\neg Shaves(Barber, x)\ \lor\ \neg Shaves(x, x)$ for each $x$, one of the form $Shaves(Barber, x)\ \lor\ Shaves(x, x)$ for each $x$, and one last clause $Shaves(Someone, Barber)$. Thus, if there are $n$ people ($n$ possible values of $x$), the CNF form has $2n+1$ clauses in it.

Finally, note that the Barber is one of those $n$ people. Thus, for the clauses corresponding to the case $x=Barber$, we get a clause $\neg Shaves(Barber, Barber)\ \lor\ \neg Shaves(Barber, Barber)$ and a clause $Shaves(Barber, Barber)\ \lor\ Shaves(Barber, Barber)$. Now you should be able to find a contradiction in there.

StackExchange Computer Science Q#93540, answer score: 5