satisfiability stuff for propositionsl formulas

 * "atom_union" now has the same type signature with Harrison's
implementation
 * abstract "onValuations" function to define functions like
"onallvaluations" easily
 * "atoms", "tautology", "unsatisfiable", "satisfiable" as in
"atp_interactive.ml"