I understand that elimination is:
p v q
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.
Philosophy Stack Exchange is a question and answer site for those interested in the study of the fundamental nature of knowledge, reality, and existence. It only takes a minute to sign up.Sign up to join this community
Natural deduction and resolution are two approaches to theorem proving. Consider the following premises:
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
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.
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