Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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?

share|improve this question

1 Answer 1

up vote 1 down vote accepted

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.

share|improve this answer
    
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 at 17:21
    
Np. I'm glad you figured it out. –  Hunan Rostomyan Apr 30 at 18:10

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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