Simple tableaux for two expansions of Gödel modal logic

This paper considers two logics. The first one, $\mathbf{K}{\mathsf{G}}_{\mathsf{i}\mathsf{n}\mathsf{v}}$, is an expansion of the Gödel modal logic $\mathbf{K}\mathsf{G}$ with the involutive negation ${\sim }_{\mathsf{i}}$ defined as $v({\sim }_{\mathsf{i}}\phi ,w)=1-v(\phi ,w)$. The second one, $\mathbf{K}{\mathsf{G}}_{\mathsf{b}\mathsf{l}}$, is the expansion of $\mathbf{K}{\mathsf{G}}_{\mathsf{i}\mathsf{n}\mathsf{v}}$ with the bi-lattice connectives and modalities. We explore their semantical properties w.r.t. the standard semantics on $[0,1]$-valued Kripke frames and define a unified tableaux calculus that allows for the explicit countermodel construction. For this, we use an alternative semantics with the finite model property. Using the tableaux calculus, we construct a decision algorithm and show that satisfiability and validity in $\mathbf{K}{\mathsf{G}}_{\mathsf{i}\mathsf{n}\mathsf{v}}$ and $\mathbf{K}{\mathsf{G}}_{\mathsf{b}\mathsf{l}}$ are PSpace-complete.