Automated Consistency Checking of Expressive Ontologies --- Beware of the Wrong Interpretation of Success!
Christoph Benzmüller, Marco Ziener · 2013
There have been attempts to (partially) translate expressive ontologies such as SUMO or Cyc to first-order logic and to use firstorder automated theorem provers for detecting errors and inconsistencies. Claims have been made that these translation results are now ready for use within practical applications. This paper adopts a critical attitude: The fact that a translation of an expressive ontology into a target logic (be it first-order or higher-order or modal, etc.) exists for which satisfiability can be shown does not imply that the approach is ready for application. What might still be missing is a guarantee of the faithfulness of the translation. The issue is illustrated in connection with a (knowingly) unfaithful translation of SUMO into classical higher-order logic. The focus is on a small, provably satisfiable subset of this translated SUMO ontology. By adding some intuitively compatible and sound ABox axioms the unfaithfulness of the translation can easily be revealed with automated theorem provers. Without the ABox content, however, the problem remains undetected. We thus argue for the extensive integration of ABox information into automated consistency checking for expressive ontologies, in particular, when logic translations are involved and when faithfulness has not or cannot be formally ensured.