The paper presents a tableau calculus with several refinements for reasoning in the description logic SHOI. The calculus uses non-standard rules for dealing with TBox statements. Whereas in existing tableau approaches a fixed rule is used for dealing with TBox statements, the tableau calculus uses a dynamically generated set of refined rules. This approach has become practical because reasoners with flexible sets of rules can be generatedwith the tableau prover generation prototype MetTeL. We also define and investigate variations of the unrestricted blocking mechanism in which equality reasoning is realised by ordered rewriting and the application of the blocking rule is controlled by excluding its application to a fixed, finite set of individual terms. Reasoning with the unique name assumption and excluding ABox individuals from the application of blocking can be seen as two separate instances of the latter. Experiments show the refinements lead to fewer rule applications and improved performance.
|Title of host publication
|Proceedings of the 26th International Workshop on Description Logics (DL-2013)
|Thomas Eiter, Birte Glimm, Yevgeny Kazakov, Markus Krötzsch
|RWTH Aachen University
|Number of pages
|Published - 2013
|CEUR Workshop Proceedings