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 fix- point logics. Finally, some open questions. The talk is intended to be expository so it will be at a fairly high level.
| Original language | English |
|---|---|
| Journal | CEUR Workshop Proceedings |
| Volume | 477 |
| Publication status | Published - 2009 |
| Event | 22nd International Workshop on Description Logics, DL 2009 - Oxford, United Kingdom Duration: 27 Jul 2009 → 30 Jul 2009 |