@inproceedings{05ee06602bc34f38b11a37de3a17eac9,
title = "An abstract tableau calculus for the description logic SHOI using unrestricted blocking and rewriting",
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.",
author = "Mohammad Khodadadi and Schmidt, {Renate A.} and Dmitry Tishkovsky",
year = "2012",
language = "English",
volume = "846",
series = "CEUR Workshop Proceedings",
publisher = "RWTH Aachen University",
pages = "224--234",
booktitle = "CEUR Workshop Proceedings|CEUR Workshop Proc.",
address = "Germany",
note = "25th International Workshop on Description Logics, DL 2012 ; Conference date: 01-07-2012",
}