@ARTICLE{BabenyshevRybakovSchmidtTishkovsky10,
AUTHOR = {Babenyshev, S. and Rybakov, V. and Schmidt, R. A. and Tishkovsky, D.},
YEAR = {2010},
TITLE = {A Tableau Method for Checking Rule Admissibility in {S4}},
JOURNAL = {Electronic Notes in Theoretical Computer Science},
VOLUME = {262},
PAGES = {17--32},
DOI = {http://dx.doi.org/10.1016/j.entcs.2010.04.003},
ABSTRACT = {
Rules that are admissible can be used in any derivations in any axiomatic
system of a logic.
In this paper we introduce a method for checking the admissibility
of rules in the modal logic S4.
Our method is based on a standard semantic ground tableau approach.
In particular, we reduce rule admissibility in S4 to 
satisfiability of a formula in a logic that extends S4.
The extended logic is characterised by a class of models that satisfy a
variant of the co-cover property.
The class of models can be formalised by a well-defined first-order specification.
Using a recently introduced framework for synthesising tableau decision
procedures this can be turned into a sound, complete and terminating
tableau calculus for the extended logic, and gives a tableau-based
method for determining the admissibility of rules.
},
}