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 ?


1 Answer 1


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 \}$.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .