Global Caching, Inverse Roles and Fixpoint Logics

Abstract. 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 fixpoint logics. Finally, some open questions. The talk is intended to be expository so it will be at a fairly high level.

• Type: Journal
• Year: 2009
• Where: DLOG
• Authors: Rajeev Goré
• Keywords: Automated Reasoning, Caching, DLOG 2009, Global, Optimal Tableau-based Algorithm