Optimization techniques for intuitionistic propositional logic and their implementation