Global caching, inverse roles and fixpoint logics

I will begin by explaining an optimal tableau-based algorithm for checking ALC-satisfiability which uses "global caching" and which appears to work well in practice. The algorithm settles a conjecture that "global caching can lead to optimality". I will then explain how "global caching" can be extended to "global state caching" for inverse roles, thereby extending the result to ALCI-satisfiability, and converse roles in general. Finally, I will explain how "global caching" can be used to give optimal "on the fly" tableau decision procedures for some fix- point logics. Finally, some open questions. The talk is intended to be expository so it will be at a fairly high level