Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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|improve this question

1 Answer 1

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|improve this answer
    
Addition: wolframalpha.com/input/?i=%28a%E2%86%94b%29 –  Margus Apr 3 '11 at 15:24

Your Answer

 
discard

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.