@INPROCEEDINGS{KhodadadiSchmidtTishkovsky12a,
AUTHOR = {Khodadadi, M. and Schmidt, R. A. and Tishkovsky, D.},
YEAR = {2012},
TITLE = {An Abstract Tableau Calculus for the Description Logic {SHOI} Using Unrestricted Blocking and Rewriting}
EDITOR = {Kazakov, Y. and Lembo, D. and Wolter, F.},
BOOKTITLE = {Proceedings of the 2012 International Workshop on Description Logics (DL-2012)},
SERIES = {CEUR Workshop Proceedings},
VOLUME = {846},
PUBLISHER = {CEUR-WS.org},
ABSTRACT = {
This paper presents an abstract tableau calculus for the description logic SHOI.
SHOI is the extension of ALC with singleton concepts, role inverse,
transitive roles and role inclusion axioms. The presented tableau calculus is
inspired by a recently introduced tableau synthesis framework. Termination is
achieved by a variation of the unrestricted blocking mechanism that immediately
rewrites terms with respect to the conjectured equalities. This approach leads
to reduced search space for decision procedures based on the calculus. We also
discuss restrictions of the application of the blocking rule by means of
additional side conditions and/or additional premises.
}
}