Fix bug in resolve_cnf, and start work on resolve.

It turns out it is necessary to iterate over all pairs
of clauses in resolve_cnf

The resolve algorithm is working for simple examples, but
because of the necessity to iterate over pairs of clauses,
I don't know how to make it efficient when dealing with
formulas not in cnf.
Merge branch 'master' of github.com:winobes/modal-logic