Abstract
Ontologies provide the logical underpinning for the Semantic Web, but their consequences can sometimes be surprising and must be explained to users. A promising kind of explanations are proofs generated via automated reasoning. We report about a series of studies with the purpose of exploring how to explain such formal logical proofs to humans. We compare different representations, such as tree- vs. text-based visualizations, but also vary other parameters such as length, interactivity, and the shape of formulas. We did not find evidence to support our main hypothesis that different user groups can understand different proof representations better. Nevertheless, when participants directly compared proof representations, their subjective rankings showed some tendencies such as that most people prefer short tree-shaped proofs. However, this did not impact the user’s understanding of the proofs as measured by an objective performance measure.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
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: ISWC (2017). https://doi.org/10.1007/978-3-319-68288-4_2
Alrabbaa, C., Baader, F., Borgwardt, S., Dachselt, R., Koopmann, P., Méndez, J.: Evonne: interactive proof visualization for description logics (system description). In: IJCAR (2022). https://doi.org/10.1007/978-3-031-10769-6_16
Alrabbaa, C., Baader, F., Borgwardt, S., Koopmann, P., Kovtunova, A.: Finding small proofs for description logic entailments: theory and practice. In: LPAR-23 (2020). https://doi.org/10.29007/nhpp
Alrabbaa, C., Baader, F., Borgwardt, S., Koopmann, P., Kovtunova, A.: On the complexity of finding good proofs for description logic entailments. In: DL Workshop (2020). http://ceur-ws.org/Vol-2663/paper-1.pdf
Alrabbaa, C., Baader, F., Borgwardt, S., Koopmann, P., Kovtunova, A.: Finding good proofs for description logic entailments using recursive quality measures. In: CADE (2021). https://doi.org/10.1007/978-3-030-79876-5_17
Alrabbaa, C., Baader, F., Dachselt, R., Flemisch, T., Koopmann, P.: Visualising proofs and the modular structure of ontologies to support ontology repair. In: DL Workshop (2020). http://ceur-ws.org/Vol-2663/paper-2.pdf
Alrabbaa, C., Borgwardt, S., Knieriemen, N., Kovtunova, A., Rothermel, A.M., Wiehr, F.: In the hand of the beholder: comparing interactive proof visualizations. In: DL Workshop (2021). http://ceur-ws.org/Vol-2954/paper-2.pdf
Androutsopoulos, I., Lampouras, G., Galanis, D.: Generating natural language descriptions from OWL ontologies: the NaturalOWL system. JAIR 48, 671–715 (2013). https://doi.org/10.1613/jair.4017
Baader, F., Brandt, S., Lutz, C.: Pushing the \(\cal{EL} \) envelope. In: IJCAI (2005). http://ijcai.org/Proceedings/09/Papers/053.pdf
Baader, F., Horrocks, I., Lutz, C., Sattler, U.: An Introduction to Description Logic. Cambridge University Press, Cambridge (2017). https://doi.org/10.1017/9781139025355
Baader, F., Peñaloza, R., Suntisrivaraporn, B.: Pinpointing in the description logic \({{\cal{EL} }^+}\). In: KI (2007). https://doi.org/10.1007/978-3-540-74565-5_7
Baader, F., Suntisrivaraporn, B.: Debugging SNOMED CT using axiom pinpointing in the description logic \(\cal{EL} ^+\). In: KR-MED (2008). http://ceur-ws.org/Vol-410/Paper01.pdf
Borgida, A., Franconi, E., Horrocks, I.: Explaining \(\cal{ALC} \) subsumption. In: ECAI (2000). http://www.frontiersinai.com/ecai/ecai2000/pdf/p0209.pdf
Borgwardt, S., Hirsch, A., Kovtunova, A., Wiehr, F.: In the eye of the beholder: which proofs are best? In: DL Workshop (2020). http://ceur-ws.org/Vol-2663/paper-6.pdf
Cohen, J.: Statistical Power Analysis for the Behavioral Sciences. Lawrence Erlbaum Associates (1988). https://doi.org/10.4324/9780203771587
Condon, D.M., Revelle, W.: The international cognitive ability resource: development and initial validation of a public-domain measure. Intelligence 43, 52–64 (2014). https://doi.org/10.1016/j.intell.2014.01.004
Donadello, I., Dragoni, M., Eccher, C.: Explaining reasoning algorithms with persuasiveness: a case study for a behavioural change system. In: ACM Symposium on Applied Computing (2020). https://doi.org/10.1145/3341105.3373910
Engström, F., Nizamani, A.R., Strannegård, C.: Generating comprehensible explanations in description logic. In: DL Workshop (2014). http://ceur-ws.org/Vol-1193/paper_17.pdf
Flemisch, T., Langner, R., Alrabbaa, C., Dachselt, R.: Towards designing a tool for understanding proofs in ontologies through combined node-link diagrams. In: VOILA Workshop (2020). http://ceur-ws.org/Vol-2778/paper3.pdf
Hayes, A.F.: Introduction to Mediation, Moderation, and Conditional Process Analysis: A Regression-Based Approach. Guilford Publications, New York (2017). https://doi.org/10.1111/jedm.12050
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
Horridge, M., Bail, S., Parsia, B., Sattler, U.: Toward cognitive support for OWL justifications. Knowl.-Based Syst. 53, 66–79 (2013). https://doi.org/10.1016/j.knosys.2013.08.021
Horridge, M., Parsia, B., Sattler, U.: Justification oriented proofs in OWL. In: ISWC (2010). https://doi.org/10.1007/978-3-642-17746-0_23
IBM: SPSS Statistics. https://www.ibm.com/products/spss-statistics
Kalyanpur, A.: Debugging and repair of OWL ontologies. Ph.D. thesis, University of Maryland, College Park, USA (2006). http://hdl.handle.net/1903/3820
Kazakov, Y., Klinov, P., Stupnikov, A.: Towards reusable explanation services in Protege. In: DL Workshop (2017). http://www.ceur-ws.org/Vol-1879/paper31.pdf
Kazakov, Y., Krötzsch, M., Simančík, F.: The incredible ELK. J. Autom. Reason. 53(1), 1–61 (2013). https://doi.org/10.1007/s10817-013-9296-3
Kontopoulos, E., Bassiliades, N., Antoniou, G.: Visualizing semantic web proofs of defeasible logic in the DR-DEVICE system. Knowl. Based Syst. (2011). https://doi.org/10.1016/j.knosys.2010.12.001
Kuhn, T.: The understandability of OWL statements in controlled English. Semant. Web 4, 101–115 (2013). https://doi.org/10.3233/SW-2012-0063
McGuinness, D.L.: Explaining reasoning in description logics. Ph.D. thesis, Rutgers University, NJ, USA (1996). https://doi.org/10.7282/t3-q0c6-5305
Meehan, T.F., et al.: Logical development of the cell ontology. BMC Bioinform. 12, 1–12 (2011). https://doi.org/10.1186/1471-2105-12-6
Miller, T.: Explanation in artificial intelligence: insights from the social sciences. AI 267, 1–38 (2019). https://doi.org/10.1016/j.artint.2018.07.007
Nguyen, T.A.T., Power, R., Piwek, P., Williams, S.: Predicting the understandability of OWL inferences. In: ESWC (2013). https://doi.org/10.1007/978-3-642-38288-8_8
Schiller, M.R.G., Glimm, B.: Towards explicative inference for OWL. In: DL Workshop (2013). http://ceur-ws.org/Vol-1014/paper_36.pdf
Schiller, M.R.G., Schiller, F., Glimm, B.: Testing the adequacy of automated explanations of EL subsumptions. In: DL Workshop (2017). http://ceur-ws.org/Vol-1879/paper43.pdf
Schlobach, S.: Explaining subsumption by optimal interpolation. In: JELIA (2004). https://doi.org/10.1007/978-3-540-30227-8_35
Schlobach, S., Cornet, R.: Non-standard reasoning services for the debugging of description logic terminologies. In: IJCAI (2003). http://ijcai.org/Proceedings/03/Papers/053.pdf
Schulz, S.: The role of foundational ontologies for preventing bad ontology design. In: BOG Workshop (2018). http://ceur-ws.org/Vol-2205/paper22_bog1.pdf
Simancik, F., Kazakov, Y., Horrocks, I.: Consequence-based reasoning beyond Horn ontologies. In: IJCAI (2011). https://doi.org/10.5591/978-1-57735-516-8/IJCAI11-187
Acknowledgements
This work was supported by the DFG grant 389792660 as part of TRR 248 – CPEC (https://perspicuous-computing.science), and QuantLA, GRK 1763 (https://lat.inf.tu-dresden.de/quantla).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2022 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Alrabbaa, C. et al. (2022). In the Head of the Beholder: Comparing Different Proof Representations. In: Governatori, G., Turhan, AY. (eds) Rules and Reasoning. RuleML+RR 2022. Lecture Notes in Computer Science, vol 13752. Springer, Cham. https://doi.org/10.1007/978-3-031-21541-4_14
Download citation
DOI: https://doi.org/10.1007/978-3-031-21541-4_14
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-21540-7
Online ISBN: 978-3-031-21541-4
eBook Packages: Computer ScienceComputer Science (R0)