satisfiability stuff for propositional 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"
tidying up HPLAR.ATPInteractive.Formula

 * added references to line numbers in Harrison's code
 * TODO marks for some normal form functions
 * "psimplify" for simplifying propositional formulas
translations of "nnf", "nenf", "rawdnf"