What is the difference between the resolution rule and the elimination in natural deduction?

I understand that elimination is:

p v q

¬q

then p

and resolution is:

q1 v q2 v q3...qn
¬q1 v q2 v q3...qn
then q2 v q3...qn

I see no difference, but my teacher is telling us don't use the elimination method. Use resolution.

• He might be referring to using introduction/elimination rules for connectives as the "elimination method", which is how natural deduction usually goes. Resolution is not really a natural deduction rule, it requires converting everything into Robinson's clauses (disjunctions of literals) first, see Resolution. – Conifold Apr 9 at 18:54
• See Resolution rule. The first one is a particular case of the more general resolution rule; the particular one is only a different version of modus ponens. – Mauro ALLEGRANZA Apr 10 at 8:08
• What you have called "elimination" is not a "standard" Natural Deduction elimination rule. It is called disjunctive syllogism, also known as "disjunction elimination" and "or elimination". – Mauro ALLEGRANZA Apr 10 at 13:20

Natural deduction and resolution are two approaches to theorem proving. Consider the following premises:

1. ¬Q → P
2. ¬Q

The goal is to derive P. One could prove this with natural deduction using the conditional elimination rule (→E) as shown by this proof checker:

The resolution approach is different:

This resolution technique uses proof by contradiction and is based on the fact that any sentence in propositional logic can be transformed into an equivalent sentence in conjunctive normal form.

In this example the two premises above in conjunctive normal form would look like (P ∨ Q) ∧ ¬Q. The negation of the conclusion would be the clause ¬P. Using a proof by contradiction we would want to show that (P ∨ Q) ∧ ¬Q ∧ ¬P leads to the empty clause. This is similar to what the OP started with:

p v q

¬q

then p

Instead of using introduction and elimination rules as in natural deduction at this point only the resolution rule is needed. Here is how the proof might look with the resolution rule used twice:

```  P ∨ Q      ¬Q
-------------
P          ~P
--------------
X
```

The empty clause at the end, symbolized by "X", shows that the original conjunction of those three clauses was contradictory. Since we conjoined the negation of the conclusion "P", we have shown than "P" can be derived from those premises.

The OP wants to know what the difference is between resolution and natural deduction. The difference is the technique used to construct the proof. Natural deduction uses introduction and elimination inference rules while reduction first converts the premises and negation of the conclusion to conjunctive normal form and then uses the resolution rule on the clauses aiming for the empty clause.

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

Wikipedia contributors. (2019, March 22). Resolution (logic). In Wikipedia, The Free Encyclopedia. Retrieved 11:07, April 10, 2019, from https://en.wikipedia.org/w/index.php?title=Resolution_(logic)&oldid=888959771