Formulas partly support nested K and B.

* Using Maybe now everywhere.
* Added classes Belief and Knowledge.
* Quantifier grounding respects sorts now (i.e., number of same-sorted
  variables many standard names are subsituted).

Todo:
* CNF should be minimized.
* Negated clause should be added to setup before querying the nested K
  or B formula.
* Representation theorem?