Evonne: Interactive Proof Visualization for Description Logics (System Description)

Research output: Contribution to book/conference proceedings/anthology/reportChapter in book/anthology/reportContributedpeer-review

Contributors

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.

Details

Original languageEnglish
Title of host publicationProc. of the 11th International Joint Conference on Automated Reasoning
PublisherSpringer, Cham
Pages271-280
Number of pages10
Publication statusPublished - 2022
Peer-reviewedYes

Publication series

SeriesLecture Notes in Computer Science
Volume13385
ISSN0302-9743

Keywords

Research priority areas of TU Dresden

    DFG Classification of Subject Areas according to Review Boards

      Subject groups, research areas, subject areas according to Destatis