Past exam of the computer science course of the University of Oxford / 2015 / Logic and proof / 1 / b / Solution

Replace each implication by a logical disjunction and use the conjunctive normal form for exclusive or from part (a). The resulting Boolean clauses areHere the displayed array is a list of the six Boolean clauses, whose logical conjunction is equivalent to all four constraints.

Use resolution first on $I$, then on $T$, and finally on $H$:Removing the repeated Boolean literal in the final Boolean clause uses idempotence. Neither $C_4$ nor $C_6$ is needed: even the weaker assumptions that the coin has at least one outcome and that at least one person wins already force $Y$, once the two implications hold.