An admissibility criterion for inference rules with metavariables in the modal logic $S4.\alpha_N$

Using the criterion of this paper, we solve the substitution problem and obtain an algorithm for determining the solvability of logical equations in the modal logic $S4.\alpha_N$. Another corollary of the criterion is the solvability of the corresponding quasiequational theory of the free modal algebra whose signature is enriched with constants for the free generators.