On the modal logic K plus theories

K + T is the propositional modal logic K with the elements of the finite set T as additional axioms. We develop a sequent calculus that is suited for proof search in K + T and discuss methods to improve the efficiency. An implementation of the resulting decision procedure is part of the Logics Workbench LWB. Then we show that - in contrast to K, KT, S4 - there are theories T and formulas A where a counter-model must have a superpolynomial diameter in the size of T plus A. In the last part we construct an embedding of S4 in K + T.