Unchain My EL Reasoner
Yevgeny Kazakov‚ Markus Krötzsch and Frantisek Simancik
We study a restriction of the classification procedure for EL++ where the inference rule for complex role inclusion axioms (RIAs) is applied in a ``left-linear'' way in analogy with the well-known procedure for computing the transitive closure of a binary relation. We introduce a notion of left-admissibility for a set of RIAs, which specifies when a subset of RIAs can be used in a left-linear way without loosing consequences, prove a criterion which can be used to effectively check this property, and describe some preliminary experimental results analyzing when the restricted procedure can give practical improvements.
Riccardo Rosati and Sebastian Rudolph and Michael Zakharyaschev
CEUR Workshop Proceedings