Continued implementation of Representation Theorem.

* Formula::Eval() uses Formula::Reduce() now.
* Cleaned up usage of hplus, tf and the general role of names in
  methods of Formula.
* Fixed: Formula::Believe and Formula::Know negated the whole modal
  literal.