Decidability of interpretability logics ILM_0 and ILW*

The finite model property is a key step in proving decidability of modal logics. By adapting the filtration method to the generalized Veltman semantics for interpretability logics, we have been able to prove the finite model property of interpretability logic ILM_0 w.r.t. generalized Veltman models. We use the same technique to prove the finite model property of interpretability logic ILW* w.r.t. generalized Veltman models. The missing link needed to prove the decidability of ILM_0 was completeness w.r.t. generalized Veltman models, which we obtain in this article. Thus, we prove the decidability of ILM_0, which was an open problem. Using the same technique, we prove that ILW* is also decidable.