Tableau reductions: Towards an optimal decision procedure for the modal necessity

We present a new prefixed tableau system TKTK for verification of validity in modal logic KK. The system TKTK is deterministic, it uniquely generates exactly one proof tree for each clausal representation of formulas, and, moreover, it uses some syntactic reductions of prefixes. TKTK is defined in the original methodology of tableau systems, without any external technique such as backtracking, backjumping, etc. Since all the necessary bookkeeping is built into the rules, the system is not only a basis for a validity algorithm, but is itself a decision procedure. We present also a deterministic tableau decision procedure which is an extension of TKTK and can be used for the global assumptions problem.