Abstract
High-tech systems are ubiquitous and often safety and security critical: reasoning about their correctness is paramount. Thus, precise modelling and formal reasoning are necessary in order to convey knowledge unambiguously and accurately. Whilst mathematical modelling adds great rigour, it is opaque to many stakeholders which leads to errors in data handling, delays in product release, for example. This is a major motivation for the development of diagrammatic approaches to formalisation and reasoning about models of knowledge. In this paper, we present an interactive theorem prover, called iCon, for a highly expressive diagrammatic logic that is capable of modelling OWL 2 ontologies and, thus, has practical relevance. Significantly, this work is the first to design diagrammatic inference rules using insights into what humans find accessible. Specifically, we conducted an experiment about relative cognitive benefits of primitive (small step) and derived (big step) inferences, and use the results to guide the implementation of inference rules in iCon.
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
Notes
- 1.
- 2.
Available at: https://github.com/ZohrehShams/iCon.
- 3.
Any ontology reasoning task can be reduced to entailment reasoning.
- 4.
For unfamiliar readers, informally the DL syntax has the following interpretation: \(A \sqsubseteq B\): A is a subset of B; \(\perp \): the empty set; \(\exists R.A\): the set of things related to something in set A under binary relation R; \( Rang (R.A)\): the range of R is A; \( Fun (R)\): R is functional; \(\ge nR.A\): the set of things related to at least n things in A under R; \(\le nR.A\): the set of things related to at most n things in A under R.
- 5.
See https://sites.google.com/site/myardproject/exp/MateInst2.zip?aredirects=0&d=1 for full instructions.
- 6.
65.0% vs. 69.1% (Mann-Whitney \(U=179\), \(p=0.416\)) for overall (#01–20), 64.5% vs. 71.9% (\(U=179\), \(p=0.159\)) for valid transformations (#01–10), 65.5% vs. 66.2% (\(U=208\), \(p=0.958\)) for invalid ones (#11–20), 73.0% vs. 79.1% (\(U=166\), \(p=0.232\)) for valid Euler ones (#01–05), 56.0% vs. 64.8% (\(U=166.5\), \(p=0.242\)) for valid concept ones (#06–10), 52.0% vs. 64.8% (\(U=199\), \(p=0.769\)) for invalid Euler ones (#11–15), and 69.0% vs. 67.6% (\(U=194.5\), \(p=0.673\)) for invalid concept ones (#15–20).
- 7.
Note that in ontology engineering, sets that are necessarily empty are called incoherent.
References
Baader, F., Horrocks, I., Sattler, U.: Description logics. In: Staab, S., Studer, R. (eds.) Handbook on Ontologies, pp. 21–43. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-540-92673-3_1
Barwise, J., Etchemendy, J.: Hyperproof. CSLI Publications, California (1994)
Beckert, B., Grebing, S., Böhl, F.: A usability evaluation of interactive theorem provers using focus groups. In: Canal, C., Idani, A. (eds.) SEFM 2014. LNCS, vol. 8938, pp. 3–19. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-15201-1_1
Gil, J., Howse, J., Kent, S.: Formalizing spider diagrams. In: IEEE Symposium on Visual Languages, pp. 130–137. IEEE (1999). https://doi.org/10.1109/VL.1999.795884
Harrison, J., Urban, J., Wiedijk, F.: History of interactive theorem proving. In: Handbook of the History of Logic. Vol. 9: Computational Logic, pp. 135–214. Elsevier (2014)
Hou, T., Chapman, P., Blake, A.: Antipattern comprehension: an empirical evaluation. In: Formal Ontology in Information Systems. Frontiers in Artificial Intelligence, vol. 283, pp. 211–224. IOS Press (2016). https://doi.org/10.3233/978-1-61499-660-6-211
Howse, J., Stapleton, G., Flower, J., Taylor, J.: Corresponding regions in Euler diagrams. In: Hegarty, M., Meyer, B., Narayanan, N.H. (eds.) Diagrams 2002. LNCS (LNAI), vol. 2317, pp. 76–90. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-46037-3_7
Jamnik, M.: Mathematical Reasoning with Diagrams. CSLI Publications, California (2001)
Kortenkamp, U., Richter-Gebert, J.: Using automatic theorem proving to improve the usability of geometry software. In: Mathematical User-Interfaces Workshop (2004)
Linker, S., Burton, J., Blake, A.: Measuring user comprehension of inference rules in Euler diagrams. In: Jamnik, M., Uesaka, Y., Elzer Schwartz, S. (eds.) Diagrams 2016. LNCS (LNAI), vol. 9781, pp. 32–39. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-42333-3_3
Linker, S., Burton, J., Jamnik, M.: Tactical diagrammatic reasoning. In: International Workshop on User Interfaces for Theorem Provers. Electronic Proceedings in Theoretical Computer Science, vol. 239, pp. 29–42 (2016). https://doi.org/10.4204/EPTCS.239.3
Nguyen, T.A.T., Power, R., Piwek, P., Williams, S.: Measuring the understandability of deduction rules for OWL. In: International Workshop on Debugging Ontologies and Ontology Mappings, pp. 1–12. Linköping Electronic Conference Proceedings (2012)
Paulson, L.C.: Isabelle - A Generic Theorem Prover (with a contribution by T. Nipkow), vol. 828. Springer, Heidelberg (1994). https://doi.org/10.1007/BFb0030541
Rodgers, P., Zhang, L., Purchase, H.: Wellformedness properties in Euler diagrams: which should be used? IEEE Trans. Vis. Comput. Graph. 18(7), 1089–1100 (2012). https://doi.org/10.1109/TVCG.2011.143
Sato, Y., Mineshima, K.: How diagrams can support syllogistic reasoning: an experimental study. J. Log. Lang. Inf. 24(4), 409–455 (2015). https://doi.org/10.1007/s10849-015-9225-4
Sato, Y., Ueda, K., Wajima, Y.: Strategy analysis of non-consequence inference with Euler diagrams. J. Log. Lang. Inf. 27, 61–77 (2017). https://doi.org/10.1007/s10849-017-9259-x
Shams, Z., Jamnik, M., Stapleton, G., Sato, Y.: Reasoning with concept diagrams about antipatterns in ontologies. In: Geuvers, H., England, M., Hasan, O., Rabe, F., Teschke, O. (eds.) CICM 2017. LNCS (LNAI), vol. 10383, pp. 255–271. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-62075-6_18
Shimojima, A.: Semantic Properties of Diagrams and Their Cognitive Potentials. CSLI Publications, California (2015)
Stapleton, G., Compton, M., Howse, J.: Visualizing OWL 2 using diagrams. In: IEEE Symposium on Visual Languages and Human-Centric Computing, pp. 245–253. IEEE (2017). https://doi.org/10.1109/VLHCC.2017.8103474
Stapleton, G., Howse, J., Chapman, P., Delaney, A., Burton, J., Oliver, I.: Formalizing concept diagrams. In: Visual Languages and Computing, pp. 182–187. Knowledge Systems Institute (2013)
Stapleton, G., Zhang, L., Howse, J., Rodgers, P.: Drawing Euler diagrams with circles: the theory of piercings. IEEE Trans. Vis. Comput. Graph. 17(7), 1020–1032 (2011). https://doi.org/10.1109/TVCG.2010.119
Urbas, M., Jamnik, M., Stapleton, G.: Speedith: a reasoner for spider diagrams. J. Log. Lang. Inf. 24(4), 487–540 (2015). https://doi.org/10.1007/s10849-015-9229-0
Acknowledgements
This research was funded by a Leverhulme Trust Research Project Grant (RPG-2016-082) for the project entitled Accessible Reasoning with Diagrams. The authors would like to thank Prof. John Howse, Dr Andrew Blake and Dr Ryo Takemura for their cooperation in the experiments.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this paper
Cite this paper
Shams, Z., Sato, Y., Jamnik, M., Stapleton, G. (2018). Accessible Reasoning with Diagrams: From Cognition to Automation. In: Chapman, P., Stapleton, G., Moktefi, A., Perez-Kriz, S., Bellucci, F. (eds) Diagrammatic Representation and Inference. Diagrams 2018. Lecture Notes in Computer Science(), vol 10871. Springer, Cham. https://doi.org/10.1007/978-3-319-91376-6_25
Download citation
DOI: https://doi.org/10.1007/978-3-319-91376-6_25
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-91375-9
Online ISBN: 978-3-319-91376-6
eBook Packages: Computer ScienceComputer Science (R0)