Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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:


I do:

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

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

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

Your Answer


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.