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.

Gentzen was the first to show decidability. Papers about 1990 by Jörg Hudelmaier (giving an O(n log n)-space decision procedure) and by myself (Roy Dyckhoff) should be studied by anyone interested in using such a procedure. These show (following earlier work of Vorob'ev in 1950) how to avoid loop-checking in a root-first sequent calculus search. Avoiding back-tracking is a harder problem... The appropriate calculus G4ip is covered in the standard text, Basic Proof Theory. The ILTP library at Potsdam (maintained by Jens Otten) links to implementations and classes of problems. Use of large Heyting algebras isn't really the best way to do it...

Even though you accepted Henning Makholm's answer already, this seemed likely to be of some use, and was too big for a comment, so I am posting it anyway.

I found some material related to your question on pages 33–34 of Lectures on the Curry-Howard Isomorphism by Sørensen and Urzyczyn. In particular (theorem 2.4.8 and surrounding discussion):

A [intuitionistic propositional] formula of length $n$ is valid iff it is valid in all Heyting algebras of cardinality at most $2^{2^n}$.

This might be feasible to check by hand if $n&lt3$. I think that by "length" here they mean "number of variables". They sketch the proof and refer the reader to Rasiowa and Sikorski The Mathematics of Metamathematics (Warsaw 1963) for details.

The next bit is perhaps more interesting:

From … the above theorem, it follows that intuitionistic propositional logic is decidable. But the upper bound obtained this way (double exponential space) can be improved down to polynomial space, with help of other methods, see ….

This time the reference is R. Statman. "Intuitionistic propositional logic is polynomial-space complete." Theoretical Computer Science, 9:67–72, 1979.

I hope this is of some use.