0
$\begingroup$

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?

1 Answers 1

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.

  • 0
    Addition: http://www.wolframalpha.com/input/?i=%28a%E2%86%94b%292011-04-03