Given (A => B) => C , B, prove C with resolution method

Question

So with the premises
$(A \Rightarrow B) \Rightarrow C$
$B$

It is easy to prove $C$ in the Fitch method, as in the proof below proof

Therefore I should be able to prove it using a resolution proof
$(A \Rightarrow B) \Rightarrow C$
$\neg (A \Rightarrow B) \lor C$
$\neg (\neg A \lor B) \lor C$
$(\neg \neg A \land \neg B) \lor C$
$(A \land \neg B) \lor C$
$(A \lor C) \land (\neg B \lor C)$
1. $\{A,C\}$
2. $\{\neg B, C\}$
3. $\{B\}$
4. $\{\neg C\}$
5. $\{A\}$ 1, 4
6. $\{C\}$ 2, 3
7. $\{\}$ 4, 6

So we're left with:
$\{A\}$
$\{\}$

But there is no way to get rid of the $A$. What am I doing wrong? Or is the empty set mean we've proved it even though the $A$ is still there?

The proof you link to does not prove $C$ from $(A\to B)\to C$, but from $(A\to B)\to C$ and $B$. — hmakholm left over Monica, May 01 '16 at 18:10
That's what I was trying to say. I added line breaks for clarity. — jimboweb, May 01 '16 at 18:21

score 0 · Answer 1 · answered May 02 '16 at 01:34

Okay, I get it. I was just learning how this works.

I thought you had to resolve out everything, but really you just have to reach any contradiction that leads to an empty set. So by resolving C and not C and getting an empty set I have proved it. This is based on what I learned at this link:

http://ocw.mit.edu/courses/electrical-engineering-and-computer-science/6-825-techniques-in-artificial-intelligence-sma-5504-fall-2002/lecture-notes/Lecture7FinalPart1.pdf

Given (A => B) => C , B, prove C with resolution method

1 Answers1