Is there a decision procedure for intuitionistic propositional logic? Is intutionistic propositional logic decidable? If so, what is a decision procedure for it, like tableaux for classical propositional logic? EDIT: In the first revision I mistook "predicate" for "propositional".

No, there cannot be a decision procedure for intuitionistic predicate logic. If there were, then by the double-negation translation we could use it to decide classical predicate logic, which is known to be undecidable.

(Tableaux are not a decision procedure for classical predicate logic, because it is not guaranteed to terminate in the presence of quantifiers).

* * *

**Edit:** The question was changed to speak about intuitionistic _propositional_ calculus. That is indeed decidable; one decision procedure is to search for a cut-free proof in the intuitionistic sequent calculus LJ. Since every formula in a cut-free and quantifier-free proof is a subformula of the eventual conclusion, there are only finitely many possible sequents that don't repeat formulas to the left of the turnstile, so even a brute-force proof search will terminate.