Say we have a formula in CNF like so:
$$ \{ A , A \} \{\neg A \}$$
where A can be any formula you could think of.
Abviously this formula can never be true (since $ A \land \neg A$ can never be true) , and should "resolve" to the empty clause. But if I "naively" apply the first resolution step I would get $\{A\}$ as a resolvent of the above clauses, which of course is not the empty clause.
Can someone tell me what is the correct resolvent of the above formula or how I should resolve this formula correctly ?
You should never have duplicates in your clauses, so $\{ A, A \}$ immediately becomes $\{ A \}$. This is why they are treated as sets, so as to make sure duplicates never occur!
As another example: suppose you resolve $\{ A, B \}$ with $\{ \neg A, B \}$. Then the result is $\{ B \}$, rather than $\{ B,B \}$.