# How to apply the resolution rule to $\{q;\neg q\}\{q;\neg q\}$?

How would one apply the resolution rule to $$\{q;\neg q\}\{q;\neg q\}$$? Would one obtain

1. $$\{q;\neg q\}$$?

2. $$\{q;\neg q\}$$?

3. something else?

I thought it would result in the empty set, yet it seems that it ends with the same set $$\{q;\neg q\}$$. Why?

From Wikipedia

The resolution rule in propositional logic is a single valid inference rule that produces a new clause implied by two clauses containing complementary literals. A literal is a propositional variable or the negation of a propositional variable. Two literals are said to be complements if one is the negation of the other (in the following, $$\lnot c$$ is taken to be the complement to $$c$$). The resulting clause contains all the literals that do not have complements.

### A simple example

$$\frac{a \vee b, \quad \neg a \vee c}{b \vee c}$$

In plain language: Suppose $$a$$ is false. In order for the premise $$a \vee b$$ to be true, $$b$$ must be true. Alternatively, suppose $$a$$ is true. In order for the premise $$\neg a \vee c$$ to be true, $$c$$ must be true. Therefore regardless of falsehood or veracity of $$a$$, if both premises hold, then the conclusion $$b \vee c$$ is true.

If we apply the resolution rule first to 1 and 2 deleting the couple $q$ (of 1) and $\lnot q$ (of 2), we get 3 : $\{ q; ¬q \}$.
But $\{ q; ¬q \}$ is a clause, i.e. a disjunction of literals, and the formula $q \lor \lnot q$ is a tautology.