Tableau methods are one of the main techniques that underly auto­mated reasoning for modal logics, and are implemented in an ever growing number of tools. Despite the fact that tableau algorithms work extremely well in practice, they often do not meet the known complexity bounds for the logics in question. Recently, it has been shown that optimality can be obtained for some logics while retaining practicality by using a technique called “global caching”. Here, we show that global caching is applicable to all logics that can be equipped with coalgebraic semantics, for example, classical modal logic, graded modal logic, probabilistic modal logic and coalition logic. In particular, the coalgebraic approach also covers logics that combine these various features. We thus show that global caching is a widely applicable technique and also provide foundations for optimal tableau algorithms that uniformly apply to a large class of modal logics. 
Technically, we give a sound and complete tableau calculus for coal­gebraic modal logics in the presence of global assumptions, and obtain an EXPTIME upper bound by translating the satis.ability problem to reachability games. Based on the completness of the tableau calculus, we then introduce two concrete algorithms to decide satis.ability. Both algorithms are proved correct coinductively, and can be seen to gener­alise ancestor equality blocking, and global caching, respectively. Apart from giving a coinductive reconstruction of ancestor equality blocking and global caching, this showcases the wide applicability of both and demon­strates that automated reasoning with coalgebraic logics in the presence of global assumptions is also in practice not (much) harder than for modal logics with an underlying relational semantics. 
1