0

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:

enter image description here

After several steps the result was the following:

enter image description here

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?

minerals
  • 418

1 Answers1

1

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.

Noah Schweber
  • 245,398
  • Is there any specific intuition behind when to apply resolution to 1,2 2,4 3,4...? It looks pretty random to me. – minerals May 23 '15 at 20:43
  • 1
    Well, you just look for places where resolution could occur - that is, times when you have statements of the form "$A\vee . . .$" and "$\neg A\vee . . . $". Basically, it's always a good idea to resolve when you can. – Noah Schweber May 23 '15 at 20:52
  • By the way, the proof can be recast as a proof by cases (on $P\vee Q$ - in the $P$ case, use resolution on $P, \neg P\vee R$ and similarly in the $Q$ case). I think in general it makes things easier to understand if we avoid unnecessary proof by contradiction, and there are even philosophical/mathematical reasons to do so. – Noah Schweber May 23 '15 at 20:53