I'm wondering how could one transform an IFF statement in clauses for proof by resolution. Taking a <-> b for IFF a THEN b, I've come up with
a <-> b = (a -> b) && (b -> a) which then can be turned in the following 2 clauses
!a || b !b || a
But applying resolution here would obviously break everything. Is it possible to prove by resolution a statement containing an IFF? If so, in what clauses shall it be turned?