Cut-free tableau calculi for some intuitionistic modal logics
Kripke-style cut-free calculi (explicitly reflecting the structure of possible worlds) are presented for intuitionistic analogues of the modal systems K, D, T.
scientific article; zbMATH DE number 1117766