{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,15]],"date-time":"2026-07-15T00:00:38Z","timestamp":1784073638673,"version":"3.55.0"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030798758","type":"print"},{"value":"9783030798765","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,5]],"date-time":"2021-07-05T00:00:00Z","timestamp":1625443200000},"content-version":"vor","delay-in-days":185,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Logic-based approaches to AI have the advantage that their behavior can in principle be explained to a user. If, for instance, a Description Logic reasoner derives a consequence that triggers some action of the overall system, then one can explain such an entailment by presenting a proof of the consequence in an appropriate calculus. How comprehensible such a proof is depends not only on the employed calculus, but also on the properties of the particular proof, such as its overall size, its depth, the complexity of the employed sentences and proof steps, etc. For this reason, we want to determine the complexity of generating proofs that are below a certain threshold w.r.t. a given measure of proof quality. Rather than investigating this problem for a fixed proof calculus and a fixed measure, we aim for general results that hold for wide classes of calculi and measures. In previous work, we first restricted the attention to a setting where proof size is used to measure the quality of a proof. We then extended the approach to a more general setting, but important measures such as proof depth were not covered. In the present paper, we provide results for a class of measures called recursive, which yields lower complexities and also encompasses proof depth. In addition, we close some gaps left open in our previous work, thus providing a comprehensive picture of the complexity landscape.<\/jats:p>","DOI":"10.1007\/978-3-030-79876-5_17","type":"book-chapter","created":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T09:20:19Z","timestamp":1625649619000},"page":"291-308","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Finding Good Proofs for Description Logic Entailments using Recursive Quality Measures"],"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-0001-5999-2583","authenticated-orcid":false,"given":"Patrick","family":"Koopmann","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9936-0943","authenticated-orcid":false,"given":"Alisa","family":"Kovtunova","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2021,7,5]]},"reference":[{"key":"17_CR1","doi-asserted-by":"publisher","unstructured":"Alharbi, E., Howse, J., Stapleton, G., Hamie, A., Touloumis, A.: The efficacy of OWL and DL on user understanding of axioms and their entailments. In: d\u2019Amato, C., Fern\u00e1ndez, M., Tamma, V.A.M., L\u00e9cu\u00e9, F., Cudr\u00e9-Mauroux, P., Sequeda, J.F., Lange, C., Heflin, J. (eds.) ISWC 2017 - 16th International Semantic Web Conference, Proceedings. Lecture Notes in Computer Science, vol. 10587, pp. 20\u201336. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-68288-4_2","DOI":"10.1007\/978-3-319-68288-4_2"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"Alrabbaa, C., Baader, F., Borgwardt, S., Koopmann, P., Kovtunova, A.: Finding small proofs for description logic entailments: Theory and practice. In: Albert, E., Kovacs, L. (eds.) LPAR-23: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning. EPiC Series in Computing, vol. 73, pp. 32\u201367. EasyChair (2020). https:\/\/doi.org\/10.29007\/nhpp","DOI":"10.29007\/nhpp"},{"key":"17_CR3","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":"17_CR4","unstructured":"Alrabbaa, C., Baader, F., Borgwardt, S., Koopmann, P., Kovtunova, A.: Finding good proofs for description logic entailments using recursive quality measures (extended technical report) (2021), https:\/\/arxiv.org\/abs\/2104.13138, arXiv:2104.13138 [cs.AI]"},{"key":"17_CR5","unstructured":"Alrabbaa, C., Baader, F., Dachselt, R., Flemisch, T., Koopmann, P.: Visualising proofs and the modular structure of ontologies to support ontology repair. In: DL 2020: International Workshop on Description Logics. CEUR Workshop Proceedings, vol. 2663. CEUR-WS.org (2020), http:\/\/ceur-ws.org\/Vol-2663\/paper-2.pdf"},{"key":"17_CR6","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1016\/j.inffus.2019.12.012","volume":"58","author":"AB Arrieta","year":"2020","unstructured":"Arrieta, A.B., Diaz-Rodriguez, N., Ser, J.D., Bennetot, A., Tabik, S., Barbado, A., Garcia, S., Gil-Lopez, S., Molina, D., Benjamins, R., Chatila, R., Herrera, F.: Explainable Artificial Intelligence (XAI): Concepts, taxonomies, opportunities and challenges toward responsible AI. Information Fusion 58, 82\u2013115 (2020). https:\/\/doi.org\/10.1016\/j.inffus.2019.12.012","journal-title":"Information Fusion"},{"key":"17_CR7","unstructured":"Baader, F., Brandt, S., Lutz, C.: Pushing the $$\\cal{EL}$$ envelope. In: Kaelbling, L.P., Saffiotti, A. (eds.) Proc. of the 19th Int. Joint Conf. on Artificial Intelligence (IJCAI\u201905). pp. 364\u2013369. Professional Book Center (2005), http:\/\/ijcai.org\/Proceedings\/09\/Papers\/053.pdf"},{"key":"17_CR8","unstructured":"Baader, F., Brandt, S., Lutz, C.: Pushing the $$\\cal{EL}$$ envelope further. In: Clark, K., Patel-Schneider, P.F. (eds.) Proc. of the 4th Workshop on OWL: Experiences and Directions. pp. 1\u201310 (2008), http:\/\/webont.org\/owled\/2008dc\/papers\/owled2008dc_paper_3.pdf"},{"key":"17_CR9","doi-asserted-by":"publisher","DOI":"10.1017\/9781139025355","author":"F Baader","year":"2017","unstructured":"Baader, F., Horrocks, I., Lutz, C., Sattler, U.: An Introduction to Description Logic. Cambridge University Press (2017). https:\/\/doi.org\/10.1017\/9781139025355","journal-title":"Cambridge University Press"},{"key":"17_CR10","unstructured":"Baader, F., Suntisrivaraporn, B.: Debugging SNOMED CT using axiom pinpointing in the description logic $$\\cal{EL}^+$$. In: Proc. of the 3rd Conference on Knowledge Representation in Medicine (KR-MED\u201908): Representing and Sharing Knowledge Using SNOMED. CEUR-WS, vol. 410 (2008), http:\/\/ceur-ws.org\/Vol-410\/Paper01.pdf"},{"key":"17_CR11","unstructured":"Borgida, A., Franconi, E., Horrocks, I.: Explaining $$\\cal{ALC}$$ subsumption. In: ECAI 2000, Proceedings of the 14th European Conference on Artificial Intelligence, Berlin, Germany, August 20\u201325, 2000. pp. 209\u2013213 (2000), http:\/\/www.frontiersinai.com\/ecai\/ecai2000\/pdf\/p0209.pdf"},{"key":"17_CR12","doi-asserted-by":"publisher","unstructured":"Fiedler, A.: Natural language proof explanation. In: Mechanizing Mathematical Reasoning, Essays in Honor of J\u00f6rg H. Siekmann on the Occasion of His 60th Birthday. pp. 342\u2013363 (2005). https:\/\/doi.org\/10.1007\/978-3-540-32254-2_20","DOI":"10.1007\/978-3-540-32254-2_20"},{"issue":"2","key":"17_CR13","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1016\/0166-218X(93)90045-P","volume":"42","author":"G Gallo","year":"1993","unstructured":"Gallo, G., Longo, G., Pallottino, S.: Directed hypergraphs and applications. Discrete Applied Mathematics 42(2), 177\u2013201 (1993). https:\/\/doi.org\/10.1016\/0166-218X(93)90045-P","journal-title":"Discrete Applied Mathematics"},{"key":"17_CR14","unstructured":"Horridge, M.: Justification Based Explanation in Ontologies. Ph.D. thesis, University of Manchester, UK (2011), https:\/\/www.research.manchester.ac.uk\/portal\/files\/54511395\/FULL_TEXT.PDF"},{"key":"17_CR15","doi-asserted-by":"publisher","unstructured":"Horridge, M., Bail, S., Parsia, B., Sattler, U.: Toward cognitive support for OWL justifications. Knowl. Based Syst. 53, 66\u201379 (2013). https:\/\/doi.org\/10.1016\/j.knosys.2013.08.021, https:\/\/doi.org\/10.1016\/j.knosys.2013.08.021","DOI":"10.1016\/j.knosys.2013.08.021"},{"key":"17_CR16","doi-asserted-by":"publisher","unstructured":"Horridge, M., Parsia, B., Sattler, U.: Justification oriented proofs in OWL. In: The Semantic Web - ISWC 2010 - 9th International Semantic Web Conference, ISWC 2010, Shanghai, China, November 7\u201311, 2010, Revised Selected Papers, Part I. pp. 354\u2013369 (2010). https:\/\/doi.org\/10.1007\/978-3-642-17746-0_23","DOI":"10.1007\/978-3-642-17746-0_23"},{"key":"17_CR17","doi-asserted-by":"publisher","unstructured":"Huang, X.: Reconstruction proofs at the assertion level. In: Proceedings of the 12th International Conference on Automated Deduction. p. 738\u2013752. CADE-12, Springer-Verlag (1994). https:\/\/doi.org\/10.1007\/3-540-58156-1_53","DOI":"10.1007\/3-540-58156-1_53"},{"key":"17_CR18","unstructured":"Kazakov, Y.: Consequence-driven reasoning for horn SHIQ ontologies. In: Boutilier, C. (ed.) IJCAI 2009, Proceedings of the 21st International Joint Conference on Artificial Intelligence, Pasadena, California, USA, July 11\u201317, 2009. pp. 2040\u20132045 (2009), http:\/\/ijcai.org\/Proceedings\/09\/Papers\/336.pdf"},{"key":"17_CR19","doi-asserted-by":"publisher","unstructured":"Kazakov, Y., Klinov, P.: Goal-directed tracing of inferences in $$\\cal{EL}$$ ontologies. In: Mika, P., Tudorache, T., Bernstein, A., Welty, C., Knoblock, C.A., Vrandecic, D., Groth, P.T., Noy, N.F., Janowicz, K., Goble, C.A. (eds.) Proc. of the 13th International Semantic Web Conference (ISWC 2014). Lecture Notes in Computer Science, vol. 8797, pp. 196\u2013211. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-11915-1_13","DOI":"10.1007\/978-3-319-11915-1_13"},{"key":"17_CR20","unstructured":"Kazakov, Y., Klinov, P., Stupnikov, A.: Towards reusable explanation services in Protege. In: Artale, A., Glimm, B., Kontchakov, R. (eds.) Proc. of the 30th Int. Workshop on Description Logics (DL\u201917). CEUR Workshop Proceedings, vol. 1879 (2017), http:\/\/www.ceur-ws.org\/Vol-1879\/paper31.pdf"},{"issue":"1","key":"17_CR21","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. Reasoning 53(1), 1\u201361 (2014). https:\/\/doi.org\/10.1007\/s10817-013-9296-3","journal-title":"J. Autom. Reasoning"},{"key":"17_CR22","unstructured":"Lingenfelder, C.: Structuring computer generated proofs. In: Proceedings of the 11th International Joint Conference on Artificial Intelligence. Detroit, MI, USA, August 1989. pp. 378\u2013383 (1989), http:\/\/ijcai.org\/Proceedings\/89-1\/Papers\/060.pdf"},{"key":"17_CR23","doi-asserted-by":"publisher","unstructured":"McGuinness, D.L.: Explaining Reasoning in Description Logics. Ph.D. thesis, Rutgers University, NJ, USA (1996). https:\/\/doi.org\/10.7282\/t3-q0c6-5305","DOI":"10.7282\/t3-q0c6-5305"},{"key":"17_CR24","unstructured":"Nguyen, T.A.T., Power, R., Piwek, P., Williams, S.: Measuring the understandability of deduction rules for OWL. In: Proceedings of the First International Workshop on Debugging Ontologies and Ontology Mappings, WoDOOM 2012, Galway, Ireland, October 8, 2012. pp. 1\u201312 (2012), http:\/\/www.ida.liu.se\/~patla\/conferences\/WoDOOM12\/papers\/paper4.pdf"},{"key":"17_CR25","doi-asserted-by":"publisher","unstructured":"Nguyen, T.A.T., Power, R., Piwek, P., Williams, S.: Predicting the understandability of OWL inferences. In: The Semantic Web: Semantics and Big Data, 10th International Conference, ESWC 2013, Montpellier, France, May 26\u201330, 2013. Proceedings. pp. 109\u2013123 (2013). https:\/\/doi.org\/10.1007\/978-3-642-38288-8_8","DOI":"10.1007\/978-3-642-38288-8_8"},{"key":"17_CR26","unstructured":"Schiller, M.R.G., Glimm, B.: Towards explicative inference for OWL. In: Informal Proceedings of the 26th International Workshop on Description Logics, Ulm, Germany, July 23\u201326, 2013. pp. 930\u2013941 (2013), http:\/\/ceur-ws.org\/Vol-1014\/paper_36.pdf"},{"key":"17_CR27","unstructured":"Schiller, M.R.G., Schiller, F., Glimm, B.: Testing the adequacy of automated explanations of EL subsumptions. In: Proceedings of the 30th International Workshop on Description Logics, Montpellier, France, July 18\u201321, 2017. (2017), http:\/\/ceur-ws.org\/Vol-1879\/paper43.pdf"},{"key":"17_CR28","unstructured":"Schlobach, S., Cornet, R.: Non-standard reasoning services for the debugging of description logic terminologies. In: Gottlob, G., Walsh, T. (eds.) Proc. of the 18th Int. Joint Conf. on Artificial Intelligence (IJCAI 2003). pp. 355\u2013362. Morgan Kaufmann, Acapulco, Mexico (2003), http:\/\/ijcai.org\/Proceedings\/03\/Papers\/053.pdf"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 28"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-79876-5_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T09:28:34Z","timestamp":1625650114000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-79876-5_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030798758","9783030798765"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-79876-5_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"5 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.cs.cmu.edu\/~mheule\/CADE28\/","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":"76","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":"29","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":"0","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","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","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)"}},{"value":"2 invited papers and 7 system descriptions are also included.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}