{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,15]],"date-time":"2026-07-15T00:00:40Z","timestamp":1784073640619,"version":"3.55.0"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031107689","type":"print"},{"value":"9783031107696","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T00:00:00Z","timestamp":1659312000000},"content-version":"vor","delay-in-days":212,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Explanations for description logic (DL) entailments provide important support for the maintenance of large ontologies. The \u201cjustifications\u201d 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 <jats:sc>Evonne<\/jats:sc>, 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 <jats:italic>signature-based proof condensation<\/jats:italic>. Moreover, we evaluate the quality of generated proofs using real ontologies.<\/jats:p>","DOI":"10.1007\/978-3-031-10769-6_16","type":"book-chapter","created":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T01:02:56Z","timestamp":1659315776000},"page":"271-280","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Evonne: Interactive Proof Visualization for\u00a0Description Logics (System Description)"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2925-1765","authenticated-orcid":false,"given":"Christian","family":"Alrabbaa","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4049-221X","authenticated-orcid":false,"given":"Franz","family":"Baader","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0924-8478","authenticated-orcid":false,"given":"Stefan","family":"Borgwardt","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2176-876X","authenticated-orcid":false,"given":"Raimund","family":"Dachselt","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5999-2583","authenticated-orcid":false,"given":"Patrick","family":"Koopmann","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1029-7656","authenticated-orcid":false,"given":"Juli\u00e1n","family":"M\u00e9ndez","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2022,8,1]]},"reference":[{"key":"16_CR1","doi-asserted-by":"publisher","unstructured":"Alrabbaa, C., Baader, F., Borgwardt, S., Dachselt, R., Koopmann, P., M\u00e9ndez, J.: Evonne: interactive proof visualization for description logics (system description) - extended version (2022). https:\/\/doi.org\/10.48550\/ARXIV.2205.09583","DOI":"10.48550\/ARXIV.2205.09583"},{"key":"16_CR2","doi-asserted-by":"publisher","unstructured":"Alrabbaa, C., Baader, F., Borgwardt, S., Dachselt, R., Koopmann, P., M\u00e9ndez, J.: Evonne: interactive proof visualization for description logics (system description) - IJCAR22 - resources, May 2022. https:\/\/doi.org\/10.5281\/zenodo.6560603","DOI":"10.5281\/zenodo.6560603"},{"key":"16_CR3","doi-asserted-by":"publisher","unstructured":"Alrabbaa, C., Baader, F., Borgwardt, S., Koopmann, P., Kovtunova, A.: Finding small proofs for description logic entailments: theory and practice. In: Albert, E., Kov\u00e1cs, L. (eds.) Proceedings of the 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2020). EPiC Series in Computing, vol. 73, pp. 32\u201367. EasyChair (2020). https:\/\/doi.org\/10.29007\/nhpp","DOI":"10.29007\/nhpp"},{"key":"16_CR4","unstructured":"Alrabbaa, C., Baader, F., Borgwardt, S., Koopmann, P., Kovtunova, A.: On the complexity of finding good proofs for description logic entailments. In: Borgwardt, S., Meyer, T. (eds.) Proceedings of the 33rd International Workshop on Description Logics (DL 2020). CEUR Workshop Proceedings, vol. 2663. CEUR-WS.org (2020). http:\/\/ceur-ws.org\/Vol-2663\/paper-1.pdf"},{"key":"16_CR5","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-030-79876-5_17","volume-title":"Automated Deduction \u2013 CADE 28","author":"C Alrabbaa","year":"2021","unstructured":"Alrabbaa, C., Baader, F., Borgwardt, S., Koopmann, P., Kovtunova, A.: Finding good proofs for description logic entailments using recursive quality measures. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 291\u2013308. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_17"},{"key":"16_CR6","unstructured":"Alrabbaa, C., Baader, F., Dachselt, R., Flemisch, T., Koopmann, P.: Visualising proofs and the modular structure of ontologies to support ontology repair. In: Borgwardt, S., Meyer, T. (eds.) Proceedings of the 33rd International Workshop on Description Logics (DL 2020). CEUR Workshop Proceedings, vol. 2663. CEUR-WS.org (2020). http:\/\/ceur-ws.org\/Vol-2663\/paper-2.pdf"},{"key":"16_CR7","unstructured":"Alrabbaa, C., Hieke, W., Turhan, A.: Counter model transformation for explaining non-subsumption in $$\\cal{EL}$$. In: Beierle, C., Ragni, M., Stolzenburg, F., Thimm, M. (eds.) Proceedings of the 7th Workshop on Formal and Cognitive Reasoning. CEUR Workshop Proceedings, vol. 2961, pp. 9\u201322. CEUR-WS.org (2021). http:\/\/ceur-ws.org\/Vol-2961\/paper_2.pdf"},{"key":"16_CR8","doi-asserted-by":"publisher","DOI":"10.1017\/9781139025355","volume-title":"An Introduction to Description Logic","author":"F Baader","year":"2017","unstructured":"Baader, F., Horrocks, I., Lutz, C., Sattler, U.: An Introduction to Description Logic. Cambridge University Press, Cambridge (2017). https:\/\/doi.org\/10.1017\/9781139025355"},{"key":"16_CR9","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/978-3-540-32254-2_20","volume-title":"Mechanizing Mathematical Reasoning","author":"A Fiedler","year":"2005","unstructured":"Fiedler, A.: Natural language proof explanation. In: Hutter, D., Stephan, W. (eds.) Mechanizing Mathematical Reasoning. LNCS (LNAI), vol. 2605, pp. 342\u2013363. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-32254-2_20"},{"key":"16_CR10","unstructured":"Flemisch, T., Langner, R., Alrabbaa, C., Dachselt, R.: Towards designing a tool for understanding proofs in ontologies through combined node-link diagrams. In: Ivanova, V., Lambrix, P., Pesquita, C., Wiens, V. (eds.) Proceedings of the Fifth International Workshop on Visualization and Interaction for Ontologies and Linked Data (VOILA 2020). CEUR Workshop Proceedings, vol. 2778, pp. 28\u201340. CEUR-WS.org (2020). http:\/\/ceur-ws.org\/Vol-2778\/paper3.pdf"},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/3-540-48660-7_10","volume-title":"Automated Deduction \u2014 CADE-16","author":"H Horacek","year":"1999","unstructured":"Horacek, H.: Presenting proofs in a human-oriented way. In: CADE 1999. LNCS (LNAI), vol. 1632, pp. 142\u2013156. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48660-7_10"},{"key":"16_CR12","unstructured":"Horridge, M., Parsia, B., Sattler, U.: Explanation of OWL entailments in Protege 4. In: Bizer, C., Joshi, A. (eds.) Proceedings of the Poster and Demonstration Session at the 7th International Semantic Web Conference (ISWC 2008). CEUR Workshop Proceedings, vol. 401. CEUR-WS.org (2008). http:\/\/ceur-ws.org\/Vol-401\/iswc2008pd_submission_47.pdf"},{"key":"16_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-642-17746-0_23","volume-title":"The Semantic Web \u2013 ISWC 2010","author":"M Horridge","year":"2010","unstructured":"Horridge, M., Parsia, B., Sattler, U.: Justification oriented proofs in OWL. In: Patel-Schneider, P.F., Pan, Y., Hitzler, P., Mika, P., Zhang, L., Pan, J.Z., Horrocks, I., Glimm, B. (eds.) ISWC 2010. LNCS, vol. 6496, pp. 354\u2013369. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17746-0_23"},{"key":"16_CR14","unstructured":"Hyland, I., Schmidt, R.A.: Prot\u00e9g\u00e9-TS: An OWL ontology term selection tool. In: Borgwardt, S., Meyer, T. (eds.) Proceedings of the 33rd International Workshop on Description Logics (DL 2020). CEUR Workshop Proceedings, vol. 2663. CEUR-WS.org (2020). http:\/\/ceur-ws.org\/Vol-2663\/paper-12.pdf"},{"key":"16_CR15","unstructured":"Kazakov, Y., Klinov, P., Stupnikov, A.: Towards reusable explanation services in protege. In: Artale, A., Glimm, B., Kontchakov, R. (eds.) Proceedings of the 30th International Workshop on Description Logics (DL 2017). CEUR Workshop Proceedings, vol. 1879. CEUR-WS.org (2017). http:\/\/ceur-ws.org\/Vol-1879\/paper31.pdf"},{"issue":"1","key":"16_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-013-9296-3","volume":"53","author":"Y Kazakov","year":"2014","unstructured":"Kazakov, Y., Kr\u00f6tzsch, M., Simancik, F.: The incredible ELK - from polynomial procedures to efficient reasoning with $$\\cal{EL}$$ ontologies. J. Autom. Reason. 53(1), 1\u201361 (2014). https:\/\/doi.org\/10.1007\/s10817-013-9296-3","journal-title":"J. Autom. Reason."},{"issue":"3","key":"16_CR17","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/s13218-020-00655-w","volume":"34","author":"P Koopmann","year":"2020","unstructured":"Koopmann, P.: LETHE: forgetting and uniform interpolation for expressive description logics. K\u00fcnstliche Intell. 34(3), 381\u2013387 (2020). https:\/\/doi.org\/10.1007\/s13218-020-00655-w","journal-title":"K\u00fcnstliche Intell."},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"552","DOI":"10.1007\/978-3-642-45221-5_37","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P Koopmann","year":"2013","unstructured":"Koopmann, P., Schmidt, R.A.: Forgetting concept and role symbols in $$\\cal{ALCH}$$-ontologies. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 552\u2013567. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-45221-5_37"},{"key":"16_CR19","doi-asserted-by":"publisher","unstructured":"Matentzoglu, N., Parsia, B.: Bioportal snapshot 30.03.2017, March 2017. https:\/\/doi.org\/10.5281\/zenodo.439510","DOI":"10.5281\/zenodo.439510"},{"key":"16_CR20","doi-asserted-by":"publisher","unstructured":"Reger, G., Suda, M.: Checkable proofs for first-order theorem proving. In: Reger, G., Traytel, D. (eds.) 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (ARCADE 2017). EPiC Series in Computing, vol. 51, pp. 55\u201363. EasyChair (2017). https:\/\/doi.org\/10.29007\/s6d1","DOI":"10.29007\/s6d1"},{"key":"16_CR21","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-319-94205-6_2","volume-title":"Automated Reasoning","author":"Y Zhao","year":"2018","unstructured":"Zhao, Y., Schmidt, R.A.: FAME: an automated tool for semantic forgetting in expressive description logics. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 19\u201327. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_2"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-10769-6_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T01:14:14Z","timestamp":1659316454000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-10769-6_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031107689","9783031107696"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-10769-6_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"1 August 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Haifa","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Israel","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 August 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 August 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/easychair.org\/smart-program\/FLoC2022\/IJCAR-index.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"85","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"32","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"38% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.2","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5.2","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}