# Proof by resolution and IFF

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?

-

You can write it both as a CNF and as a DNF: $$(a \leftrightarrow b) \Leftrightarrow (a \land b) \lor (\lnot a \land \lnot b) \Leftrightarrow (a \lor \lnot b) \land (\lnot a \lor b).$$ For resolution you might want the negation: $$\lnot (a \leftrightarrow b) \Leftrightarrow (a \land \lnot b) \lor (\lnot a \land b) \Leftrightarrow (a \lor b) \land (\lnot a \lor \lnot b).$$ In general, every statement can be converted to a CNF or a DNF, so resolution can be used to prove (or rather, refute) every possible statement.