Extracting finite sets of entailments from OWL ontologies

The canonical standard description logic reasoning service is classification, that is, the generation of the set of atomic subsumptions which are entailed by some ontology. While this consequence relation is well defined and finite, there is significant variance in the composition of that set. For example, it is common (in tools and in discussion) to exclude some tautologies (e.g., A ?, A ? A). While for many purposes such divergences are harmless, there are many for which precision about what appears in the classification is essential, for example, estimating differences in logical content. In this paper, we propose definitions for different types of finite entailment sets of an OWL ontology based on the transitive closure and transitive reduction of its asserted and inferred class graphs. The purpose of this work is to introduce a flexible and extensible specification for selecting a particular set of entailments, with the aim of ensuring the correctness and replicability of OWL-based applications.