OL solver and tactic

Created by: SimonGuilloud

New Tautology tactic and solver for propositional logic. Simpler and much more effective than the previous sequent calculus based solver.