I have never had logic classes so I always struggle with the assignments that concern this interesting field. I was reading the slides about resolution theorem proving and there was a step-by-step explanation of how to prove the following example:
After several steps the result was the following:
After reading through the complete proof I understood that I do not understand the meaning of "resolve" in "By resolving away Q in lines 5 and 7, we get R". I know it is a very trivial question, but what does "resolve away" literally mean?
Here's how to think about it colloquially: $\neg Q\vee R$ is a problem - does $\neg Q$ hold or does $R$ hold? - and the hypothesis $Q$ resolves the problem, resulting in a formula ("$R$") not containing $Q$.
Technically, this is an example of "resolution": http://en.wikipedia.org/wiki/Resolution_inference. The notation is a bit weird, but what's going on is this:
$\Gamma$ is a set of formulas, and we think of $\Gamma$ as being the disjunction of those formulas. So, for example, $\{P, Q, R\}$ means $P\vee Q\vee R$. If $\Gamma\subset\Gamma'$ then $\Gamma'$ is weaker than $\Gamma$.
In particular, "$\Gamma\cup\{\varphi\}$" means "One of the statements in $\Gamma$ is true, or $\varphi$ is true.
If $\Gamma_1, \Gamma_2, \Gamma_3$ are sets of formulas, then $${\Gamma_1 \quad \Gamma_2 \over \Gamma_3}$$ means "from $\Gamma_1$ and $\Gamma_2$ we can deduce $\Gamma_3$."
The "$\vert l \vert$" off to the side is just a bookkeeping device.
NOTE: there are many different ways to present formal proofs; I find the one in the wikipedia page I cited very unusual. The two (or three) column proof method you use is much simpler, albeit annoyingly long and sometimes hard to read; natural deduction http://en.wikipedia.org/wiki/Natural_deduction strikes a nice balance.