# 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.