1

This is my first real stab at Resolution refutation. I'm given: "Heads, I win. Tails, you lose. Prove I win" and I'm supposed to solve with resolution refutation. I add the following (The original problem states I can do this to make it solvable) statements to the premises: Heads I don't lose, Tails You don't win, The coin can only be heads or tails, If I lose you win, If you lose I win.

So I make the initial pre-conditions:

{~H,Wi}
{~T,Ly}
{~H,~Li}
{~T,~Wy}
{~Ly,Wi}
{~Li,Wy}
{~HT,~TH}
{~Wi}

I do:

{~H} 1,8
{~Ly} 5,8
{~T}
{} 7,9,10

Is this legal? How should I have approached this problem?

jason dancks
  • 113

1 Answers1

1

Given: $P \equiv (H \rightarrow \lnot Li) \land (T \rightarrow \lnot Wy) \land (H \lor T) \land (Li \rightarrow Wy) \land (Ly \rightarrow Wi)$, we want to refute $(P \land \lnot Wi)$ by the method of resolution. We can't, however, because $(P \land \lnot Wi)$ is satisfiable. Consider, for example, the assignment $v(H) = \top, v(\phi) = \bot$ for all $\phi \not= H$. Something is missing.

Hunan Rostomyan
  • 2,055
  • I got it. I add the statements: "Not heads implies tails" and "not tails implies heads". Combined with the other statements this leads to the empty set provided this is legal: {~T},{~H},{H,T} -> {}. It wasn't satisfiable because it wasn't fully constrained. Thank you for your help Hunan. – jason dancks Apr 30 '14 at 17:21
  • Np. I'm glad you figured it out. – Hunan Rostomyan Apr 30 '14 at 18:10