The generation of proof certificates and the use of proof
checkers is nowadays standard in first-order automated theorem prov-
ing and related areas. They have, to the best of our knowledge, not yet
been employed in Description Logics, where the focus was on detecting
and repairing errors in the ontology, rather than on catching erroneous
consequences created by an incorrect reasoner. This paper reports on
first steps towards remedying this deficit for subsumptions computed by
the DL reasoner Elk. We use an existing tool for generating proofs of
consequences from Elk, and transform these proofs into a format that
is accepted as certificates by our proof checker. The checker is obtained
as an instance of a generic certification tool based on the Logical Frame-
work with Side Conditions (LFSC), by formalizing the inference rules of
Elk in LFSC. We report on the results of applying this approach to the
classification of a large number of real-world OWL 2 EL ontologies.