@INPROCEEDINGS{KhodadadiSchmidtTishkovsky13a,
AUTHOR = {Khodadadi, M. and Schmidt, R. A. and Tishkovsky, D.},
YEAR = {2013},
TITLE = {A Refined Tableau Calculus with Controlled Blocking for the Description Logic $\mathcal SHOI$},
EDITOR = {Galmiche, D. and Larchey-Wendling, D.},
BOOKTITLE = {Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2013)},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {8123},
PUBLISHER = {Springer},
PAGES = {188--202},
DOI = {http://dx.doi.org/10.1007/978-3-642-40537-2_17},
URL = {http://www.cs.man.ac.uk/~schmidt/publications/KhodadadiSchmidtTishkovsky13a.html},
ABSTRACT = {
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, we use a dynamically generated set of
refined rules. This approach has become practical
because reasoners with flexible sets of rules can be generated
with 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.
}
}