Computing Horn Rewritings of Description Logics Ontologies

TL;DR

This paper investigates how to rewrite complex description logic ontologies into Horn form to enable more efficient reasoning, identifying conditions for such rewritings and demonstrating their applicability to real-world ontologies.

Contribution

It introduces conditions for the existence of polynomial-size Horn rewritings of description logic ontologies and extends rewriting techniques to more expressive logic programs.

Findings

Many real-world ontologies satisfy the sufficient conditions for Horn rewritings.

The proposed conditions ensure polynomial-size rewritings, facilitating tractable reasoning.

Decidability is shown to fail for certain expressive description logics, guiding the scope of the approach.

Abstract

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.