It is well known that further Hilbert axioms can be added to \Kt\ to capture
corresponding classes of Kripke frames \cite{kracht-power}.
For example the axioms
T: $\WhtBox A \to A$,
D: $\WhtBox A \to \WhtDia A$,
4: $\WhtBox A \to \WhtBox \WhtBox A$,
5: $\WhtDia \WhtBox A \to \WhtBox A$ and
B: $A \to \WhtBox \WhtDia A $
correspond to the conditions of reflexivity, seriality, transitivity,
euclideaness and symmetry.
Kracht \cite{kracht-power} has shown that we can augment \dKt\
with such axioms by adding them as structural rules, and retain soundness,
completeness and cut-elimination.
For example, the rules shown below capture these axioms exactly:

\begin{center}
\hfill
(T)\slrule {\bullet X \vdash Z} {X \vdash Z}
\hfill
(D)\slrule {* \bullet * I \vdash Z} {I \vdash Z}
\hfill
(4)\slrule {\bullet X \vdash Z} {\bullet \bullet X \vdash Z}
\hfill \mbox{}
\end{center}

\begin{center}
\hfill
(5)\slrule {* \bullet * X \vdash Z} {\bullet * \bullet * X \vdash Z}
\hfill
(B)\slrule {* \bullet * (* \bullet * X; Y) \vdash Z}
  {X;  * \bullet * Y \vdash Z}
\hfill \mbox{}
\end{center}

Consequently, we can trivially extend \dKt\,
and hence our implementation, to capture many extensions of
the tense logic \Kt (see \cite{kracht-power}).