First Results on How to Certify Subsumptions Computed by the ๐๐ Reasoner ELK Using the Logical Framework with Side Conditions
Research output: Contribution to book/conference proceedings/anthology/report โบ Conference contribution โบ Contributed โบ peer-review
Contributors
Abstract
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.
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.
Details
Original language | English |
---|---|
Title of host publication | Proceedings of the 33rd International Workshop on Description Logics (DL 2020) |
Publisher | CEUR-WS |
Publication status | Published - 2020 |
Peer-reviewed | Yes |
Publication series
Series | CEUR Workshop Proceedings |
---|---|
Volume | 2663 |
ISSN | 1613-0073 |
External IDs
ORCID | /0000-0002-4049-221X/work/142247943 |
---|