HornDL: An Expressive Horn Description Logic with PTime Data Complexity

摘要: We introduce a Horn description logic called Horn-DL, which is strictly and essentially richer than Horn-$\mathcal{SROIQ}$, while still has PTime data complexity. In comparison with HornDL additionally allows the universal role assertions of form irreflexive(s), $\lnot s(a,b)$, $a \not\doteq b$. More importantly, in contrast to all well-known fragments $\mathcal{EL}$, DL-Lite, DLP, Horn-$\mathcal{SHIQ}$, Horn-$\mathcal{SROIQ}$ logics, concept constructor "universal restriction" appear at left hand side terminological inclusion axioms. Namely, restriction can be used such places conjunction corresponding existential restriction. long version this paper, we present first algorithm complexity for checking satisfiability knowledge bases.