  In this paper we present two terminating tableau calculi for propositional
Dummett logic obeying the subformula property. The ideas of our calculi rely on
the linearly ordered Kripke semantics of Dummett logic. The first calculus
works on two semantical levels: the present and the next possible world. The
second calculus employs the usual object language of tableau systems and
exploits a property of the construction of the completeness theorem to
introduce a check which is an alternative to loop check mechanisms.
