3
$\begingroup$

I am trying to prove using the resolution technique that the following two clauses are contradicting:

  1. $\forall_x Shaves(Barber, x) \iff \neg Shaves(x, x)$
  2. $\exists_x Shaves(x, Barber)$

After turing those into the conjunctive normal form and skolemization I get the following clauses:

  1. $\neg Shaves(Barber, x)\ \lor\ \neg Shaves(x, x)$
  2. $Shaves(Barber, x)\ \lor\ Shaves(x, x)$
  3. $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?

$\endgroup$
5
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.