Deciding Propositional Intuitionistic Logic by Propositional classiscal logic methods. I read about the double negation translation (Glivenkos Translation). My question is could i somehow apply this Theorem backwards to obtain a decision algorithm for an intuitionstic logic formula ?
 A: This is an open problem, but most people don't believe so. The reasons are complexity-theoretic. 
Deciding whether a formula is a tautology of intuitionistic propositional logic (or even its $\rightarrow$-only fragment)  is known to be a PSPACE-complete problem.
PSPACE is the complexity class of all decision problems that a Turing machine can solve using a polynomial amount of space (as a function of the size of the input). PSPACE-completeness means that a method for deciding whether a formula of intuitionistic propositional logic is a tautology could easily be used to solve any other problem in the class PSPACE (for a precise definition of the word "easily").
Meanwhile, deciding whether a formula is a tautology of classical propositional logic  is known to be coNP-complete. We know that coNP is a subclass of PSPACE. 
If the double-negation translation provided an effective decision algorithm for the intuitionistic logic tautology problem, that would reduce a PSPACE-complete problem to a problem in coNP, that would prove coNP = PSPACE. Is coNP = PSPACE? Most people believe that coNP is a proper subclass of PSPACE, but nobody knows for sure. This is one of the open problems in complexity theory (you may have heard about its more famous cousin, P=?NP).
