Explanations for description logic (DL) entailments provide important support for the maintenance of large ontologies. The “justifications” usually employed for this purpose in ontology editors pinpoint the parts of the ontology responsible for a given entailment. Proofs for entailments make the intermediate reasoning steps explicit, and thus explain how a consequence can actually be derived. We present an interactive system for exploring description logic proofs, called Evonne, which visualizes proofs of consequences for ontologies written in expressive DLs. We describe the methods used for computing those proofs, together with a feature called signature-based proof condensation. Moreover, we evaluate the quality of generated proofs using real ontologies.
%0 Conference Paper
%1 6ea81cf1bb624b6293b458a01656eb63
%A Alrabbaa, Christian
%A Baader, Franz
%A Borgwardt, Stefan
%A Dachselt, Raimund
%A Koopmann, Patrick
%A Méndez, Julián
%B Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Proceedings
%C Germany
%D 2022
%E Blanchette, Jasmin
%E Kovács, Laura
%E Pattinson, Dirk
%I Springer, Berlin u. a.
%K topic_knowledge FIS_scads imported
%P 271--280
%R 10.1007/978-3-031-10769-6_16
%T Evonne: Interactive Proof Visualization for Description Logics (System Description)
%X Explanations for description logic (DL) entailments provide important support for the maintenance of large ontologies. The “justifications” usually employed for this purpose in ontology editors pinpoint the parts of the ontology responsible for a given entailment. Proofs for entailments make the intermediate reasoning steps explicit, and thus explain how a consequence can actually be derived. We present an interactive system for exploring description logic proofs, called Evonne, which visualizes proofs of consequences for ontologies written in expressive DLs. We describe the methods used for computing those proofs, together with a feature called signature-based proof condensation. Moreover, we evaluate the quality of generated proofs using real ontologies.
@inproceedings{6ea81cf1bb624b6293b458a01656eb63,
abstract = {Explanations for description logic (DL) entailments provide important support for the maintenance of large ontologies. The “justifications” usually employed for this purpose in ontology editors pinpoint the parts of the ontology responsible for a given entailment. Proofs for entailments make the intermediate reasoning steps explicit, and thus explain how a consequence can actually be derived. We present an interactive system for exploring description logic proofs, called Evonne, which visualizes proofs of consequences for ontologies written in expressive DLs. We describe the methods used for computing those proofs, together with a feature called signature-based proof condensation. Moreover, we evaluate the quality of generated proofs using real ontologies.},
added-at = {2024-11-28T16:27:18.000+0100},
address = {Germany},
author = {Alrabbaa, Christian and Baader, Franz and Borgwardt, Stefan and Dachselt, Raimund and Koopmann, Patrick and M{\'e}ndez, Juli{\'a}n},
biburl = {https://puma.scadsai.uni-leipzig.de/bibtex/2b4d6288aeefa2d767bbc14be8605279f/scadsfct},
booktitle = {Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Proceedings},
doi = {10.1007/978-3-031-10769-6_16},
editor = {Blanchette, Jasmin and Kov{\'a}cs, Laura and Pattinson, Dirk},
interhash = {b5ee7637a41478978e61c0e895f6531d},
intrahash = {b4d6288aeefa2d767bbc14be8605279f},
keywords = {topic_knowledge FIS_scads imported},
language = {English},
note = {Publisher Copyright: {\textcopyright} 2022, The Author(s).},
pages = {271--280},
publisher = {Springer, Berlin [u. a.]},
series = {Lecture Notes in Computer Science, Volume 13385},
timestamp = {2024-11-28T17:41:09.000+0100},
title = {Evonne: Interactive Proof Visualization for Description Logics (System Description)},
year = 2022
}
