This paper shows in a case study that for the development, the presentation, and the computer-assisted verification of formal ontologies the usage of higher-order languages and associated proof assistant tools is highly beneficial. This case study demonstrates that the expressive power of a higher order logic in conjunction with a well developed infrastructure for theory development and presentation facilitate the development of formal ontologies in a way that is similar to the ways in which modern object oriented programming languages and associated IDEs facilitate the development of complex software. In particular ontology development in such an environment supports (a) the formal verification of the satisfaction of the axioms of a formal ontology in a class of structures that constitute its intended interpretation; (b) the computational instantiation of specific prototypical examples/models that guide the ontology development; and (c) the formal verification of proofs by demonstrating that the claimed theorems are indeed derivable from the axioms of the theory. Parallels to software development can be drawn for two reasons: Firstly, due to the non- or semi-decidability and the complexity of sufficiently expressive languages, the process of theory development, like software development, is computer assisted rather than fully automated. Secondly, the use of a higher order logic supports modularization, object orientation, model building and other features that greatly simplify the development of complex formal ontologies.
Arnold, V.I. (1997). Mathematical Methods of Classical Mechanics. Springer.
5.
Ballarin, C. (2004). Locales and locale expressions in Isabelle/Isar. In S.Berardi, M.Coppo and F.Damiani (Eds.), Types for Proofs and Programs: International Workshop, TYPES 2003, Revised Selected Papers, Torino, Italy, April 30–May 4, 2003 (pp. 34–50). Berlin, Heidelberg: Springer.
6.
Ballarin, C. (2017). HOL/Algebra/Lattice.thy.
7.
Bateman, J.A., Borgo, S., Lüttich, K., Masolo, C. & Mossakowski, T. (2007). Ontological modularity and spatial diversity. Spatial Cognition and Computation, 7(1). doi:10.1080/13875860701337991.
8.
Belot, G. (2007). The representation of time in classical mechanics. In J.Butterfield and J.Earman (Eds.), Philosophy of Physics. Elsevier.
9.
Benzmüller, C. (2015). HOL provers for first-order modal logics – experiments. In C.Benzmüller and J.Otten (Eds.), ARQNL 2014. Automated Reasoning in Quantified Non-Classical Logics. EPiC Series in Computing (Vol. 33, pp. 37–41). EasyChair.
10.
Benzmüller, C. & Woltzenlogel Paleo, B. (2015). Higher-order modal logics: Automation and applications. In A.Paschke and W.Faber (Eds.), Reasoning Web 2015. LNCS (Vol. 9203, pp. 32–74). Berlin, Germany: Springer. (Invited paper).
11.
Bittner, T. (2018). Formal ontology of space, time, and physical entities in classical mechanics. Applied Ontology, 13(2), 135–179. doi:10.3233/AO-180195.
12.
Bittner, T. & Donnelly, M. (2006). A classification of spatio-temporal entities based on their location in space-time. In R.Meersman, Z.Tari and P.Herrero (Eds.), OTM 2006 Workshop Proceedings: International Workshop on Semantic-Based Geographical Information Systems. Lecture Notes in Computer Science (Vol. 4278, pp. 1626–1635). Berlin Heidelberg: Springer.
13.
Bittner, T. & Donnelly, M. (2007). Logical properties of foundational relations in bio-ontologies. Artificial Intelligence in Medicine, 39, 197–216. doi:10.1016/j.artmed.2006.12.005.
14.
Blanchette, J.C. (2017). Picking Nits A User’s Guide to Nitpick for Isabelle/HOL Picking Nits, A User’s Guide to Nitpick for Isabelle/HOL. Technical report, Institut für Informatik, Technische Universität München.
15.
Butterfield, J. (2007). On symplectic reduction in classical mechanics. In J.Butterfield and J.Earman (Eds.), Philosophy of Physics. Elsevier.
16.
Champollion, L. & Krifka, M. (2015). Mereology. In P.Dekker and M.Aloni (Eds.), Cambridge Handbook of Formal Semantics. Cambridge University Press.
17.
Church, A. (1940). A formulation of the simple theory of types. The Journal of Symbolic Logic, 5(2), 56–68. doi:10.2307/2266170.
18.
Church, A. (1941). The Calculi of Lambda-Conversation. Princeton, NY: Princeton University Press.
19.
Copi, I. (1979). Symbolic Logic. Upper Saddle River, NJ: Prentice Hall.
20.
Einstein, A. (1951). Relativity: The Special and the General Theory. New York: Crown Publishers Inc.
21.
Foster, S., Zeyda, F. & Woodcock, J. (2015). Isabelle/UTP: A mechanised theory engineering framework. In D.Naumann (Ed.), Unifying Theories of Programming (pp. 21–41). Cham: Springer.
22.
Gabbay, D.M. (2003). Many-Dimensional Modal Logics: Theory and Applications. North Holland: Elsevier.
23.
Gangemi, A., Guarino, N., Masolo, C., Oltramari, A. & Schneider, L. (2003). Sweetening ontologies with DOLCE. AI Magazine, 23(3), 13–24.
24.
Haarslev, V. & Möller, R. (2003). Racer: A core inference engine for the semantic web. In Proceedings of the 2nd International Workshop on Evaluation of Ontology-Based Tools (EON2003), Located at the 2nd International Semantic Web Conference ISWC 2003, Sanibel Island, Florida, USA, October 20 pp. 27–36).
25.
Horrocks, I. (1998). The FaCT system. In H.de Swart (Eds.), Automated Reasoning with Analytic Tableaux and Related Methods: International Conference Tableaux’98. Lecture Notes in Artificial Intelligenc (Vol. 1397, pp. 307–312). Springer. doi:10.1007/3-540-69778-0_30.
26.
Hughes, G. & Cresswell, M. (2004). A New Introduction to Modal Logic. London and New York: Routledge.
27.
Jones, M.P. (1993). A system of constructor classes: Overloading and implicit higher-order polymorphism. In FPCA ’93: Conference on Functional Programming and Computer Architecture, Copenhagen, Denmark (pp. 52–61). New York, NY: ACM Press. doi:10.1145/165180.165190.
28.
Jones, S.P. & Jones, M. (1997). Type classes: An exploration of the design space. Technical report.
29.
Kammüller, F., Wenzel, M. & Paulson, L.C. (1999). Locales a sectioning concept for Isabelle. In Y.Bertot, G.Dowek, L.Théry, A.Hirschowitz and C.Paulin (Eds.), Theorem Proving in Higher Order Logics: 12th International Conference, TPHOLs’ 99, Proceedings. Nice, France, September 14–17, 1999. (pp. 149–165). Berlin Heidelberg: Springer.
30.
Knublauch, H., Fergerson, R.W., Noy, N.F. & Musen, M.A. (2004). The protégé OWL plugin: An open development environment for semantic web applications. In S.A.McIlraith, D.Plexousakis and F.V.Harmelen (Eds.), Proc. Third International Semantic Web Conference, Berlin: Springer.
31.
Krifka, M. (1998). The origins of telicity. In S.Rothstein (Ed.), Events and Grammar (pp. 197–235). Netherlands, Dordrecht: Springer. doi:10.1007/978-94-011-3969-4_9.
32.
Lemon, O. & Pratt, I. (1997). Spatial Logic and the Complexity of Diagrammatic Reasoning. Machine Graphics and Vision.
Lowe, E.J. (2002). A Survey of Metaphysics. Oxford University Press.
35.
Milner, R., Tofte, M. & Harper, R. (1990). The Definition of Standard ML. MIT Press.
36.
Minkowsk, H. (1908). Die Grundgleichungen für die elektromagnetischen Vorgänge in bewegten Körpern. Nachrichten von der Gesellschaft der Wissenschaften zu Göttingen, Mathematisch-Physikalische Klasse, 53–111.
37.
Mossakowski, T., Maeder, C. & Lüttich, K. (2007). The heterogeneous tool set. In O.Grumberg and M.Huth (Eds.), TACAS 2007. Lecture Notes in Computer Science (Vol. 4424, pp. 519–522). Springer.
38.
Nipkow, T. (2003). Structured proofs in Isar/HOL. In H.Geuvers and F.Wiedijk (Eds.), Types for Proofs and Programs (TYPES 2002) (Vol. 2646, pp. 259–278). doi:10.1007/3-540-39185-1_15.
39.
Nipkow, T., Paulson, L.C. & Wenzel, M. (2002). Isabelle/HOL – a Proof Assistant for Higher-Order Logic (Vol. 2283). Springer.
40.
Norton, J.D. (2012). Einstein’s special theory of relativity and the problems in the electrodynamics of moving bodies that led him to it. In M.Janssen and C.Lehner (Eds.), Cambridge Companion to Einstein. Cambridge University Press.
41.
Paulson, L. (1995). Isabelle’s Object-Logics. Technical report, Computer Laboratory, University of Cambridge.
42.
Paulson, L. & Nipkow, T. (2017). Isabelle – a generic proof assistant. Retrieved January 19, 2018 from: http://isabelle.in.tum.de/.
43.
Paulson, L.C. (1994). Isabelle: A Generic Theorem Prover. Springer.
44.
Renz, J. & Nebel, B. (1999). On the complexity of qualitative spatial reasoning: A maximal tractable fragment of the region connection calculus. Artificial Intelligence, 108(1–2), 69–123. doi:10.1016/S0004-3702(99)00002-8.
45.
Simons, P. (1987). Parts, a Study in Ontology. Oxford: Clarendon Press.
46.
Sirin, E., Parsia, B., Grau, B.C., Kalyanpur, A. & Katz, Y. (2007). Pellet: A practical OWL-DL reasoner. Journal of Web Semantics, 5(2). doi:10.1016/j.websem.2007.03.004.
47.
Smith, B. (2003). Ontology: An introduction. In L.Floridi (Ed.), Blackwell Guide to the Philosophy of Computing and Information Blackwell Guide to the Philosophy of Computing and Information (pp. 155–166). Oxford: Blackwell.
48.
Smith, B. (2016). Basic Formal Ontology (BFO 2.0): Specification and users guide.
49.
Smith, B. & Varzi, A. (2000). Fiat and Bona fide boundaries. Philosophy and Phenomenological Research, 60(2), 401–420. doi:10.2307/2653492.
50.
Tarski, A. & Givant, S. (1999). Tarski’s system of geometry. Bulletin of Symbolic Logic, 5(2), 175–214. doi:10.2307/421089.
51.
Thompson, S. (1999). Haskell: The Craft of Functional Programming (2nd ed.). Addison-Wesley.
52.
Varzi, A. (2003). Mereology. In E.N.Zalta (Ed.), Stanford Encyclopedia of Philosophy. Stanford: CSLI (internet publication).
