Complexity of finite-variable fragments of Exptime-complete logics

摘要

The main result of the present paper is that the variable-free fragment of logic K~*, the logic with a single K-style modality and its "reflexive and transitive closure," is EXPTIME-complete. It is then shown that this immediately gives EXPTIME-completeness of variable-free fragments of a number of known EXPTIME-complete logics. Our proof contains a general idea of how to construct a polynomial-time reduction of a propositional logic to its n-variable-and even, in the cases of K~*, PDL, CTL, ATL, and some others, variable-free—fragments. Complexity of countermodels for such fragments is considered.