Computing Horn Rewritings of Description Logics Ontologies
This addresses the challenge of efficient reasoning for ontologies in AI and knowledge representation, though it is incremental as it builds on existing techniques.
The paper tackles the problem of rewriting ontologies in description logics into Horn forms to achieve tractable reasoning, showing that many real-world ontologies satisfy conditions for polynomial-size rewritings.
We study the problem of rewriting an ontology O1 expressed in a DL L1 into an ontology O2 in a Horn DL L2 such that O1 and O2 are equisatisfiable when extended with an arbitrary dataset. Ontologies that admit such rewritings are amenable to reasoning techniques ensuring tractability in data complexity. After showing undecidability whenever L1 extends ALCF, we focus on devising efficiently checkable conditions that ensure existence of a Horn rewriting. By lifting existing techniques for rewriting Disjunctive Datalog programs into plain Datalog to the case of arbitrary first-order programs with function symbols, we identify a class of ontologies that admit Horn rewritings of polynomial size. Our experiments indicate that many real-world ontologies satisfy our sufficient conditions and thus admit polynomial Horn rewritings.