Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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?

share|cite|improve this question

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.

share|cite|improve this answer
Addition: – Margus Apr 3 '11 at 15:24

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.