Propositional logic formulae parser and implementation of Tableaux method for satisfiability proving of propositional logic formulae.