let rec solve formula model =
   (* straightforward translation of the formula *)
   match formula with
      True   -> true
   |  False -> false
   | Not alpha -> not (solve alpha model)
   | Var var    -> lookup ~var model
   | And (alpha, beta) -> (solve alpha model ) && (solve beta model)
   | Or  (alpha, beta) -> (solve alpha model) || (solve beta model)
   | Implicates  (alpha, beta) -> (not (solve alpha model) ) || (solve beta model)
   | Equals (alpha, beta)  -> (solve alpha model) = (solve beta model)