{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,11]],"date-time":"2025-03-11T04:38:05Z","timestamp":1741667885282,"version":"3.38.0"},"reference-count":46,"publisher":"SAGE Publications","issue":"3","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["AO"],"published-print":{"date-parts":[[2019,8,19]]},"DOI":"10.3233\/ao-190213","type":"journal-article","created":{"date-parts":[[2019,6,21]],"date-time":"2019-06-21T15:42:14Z","timestamp":1561131734000},"page":"251-292","source":"Crossref","is-referenced-by-count":1,"title":["On the computational realization of formal ontologies: Formalizing an ontology of instantiation in spacetime using Isabelle\/HOL as a case study"],"prefix":"10.1177","volume":"14","author":[{"given":"Thomas","family":"Bittner","sequence":"first","affiliation":[{"name":"Department of Philosophy, State University of New York at Buffalo, 135 Park Hall, Buffalo, NY 14260, USA. E-mail:\u00a0bittner3@buffalo.edu"}]}],"member":"179","reference":[{"key":"10.3233\/AO-190213_ref1","unstructured":"Alexandroff, P. (1961). Elementary Concepts of Topology. New York, NY: Dover Publications."},{"key":"10.3233\/AO-190213_ref3","unstructured":"Arfken, G.B., Weber, H.J. & Harris, F.E. (2005). Mathematical Methods for Physicists, Sixth Edition: A Comprehensive Guide (6th ed.). Academic Press."},{"key":"10.3233\/AO-190213_ref4","unstructured":"Arnold, V.I. (1997). Mathematical Methods of Classical Mechanics. Springer."},{"key":"10.3233\/AO-190213_ref5","unstructured":"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\u2013May 4, 2003 (pp. 34\u201350). Berlin, Heidelberg: Springer."},{"key":"10.3233\/AO-190213_ref7","doi-asserted-by":"publisher","DOI":"10.1080\/13875860701337991"},{"key":"10.3233\/AO-190213_ref8","unstructured":"Belot, G. (2007). The representation of time in classical mechanics. In J. Butterfield and J. Earman (Eds.), Philosophy of Physics. Elsevier."},{"key":"10.3233\/AO-190213_ref9","unstructured":"Benzm\u00fcller, C. (2015). HOL provers for first-order modal logics\u00a0\u2013 experiments. In C. Benzm\u00fcller and J. Otten (Eds.), ARQNL 2014. Automated Reasoning in Quantified Non-Classical Logics. EPiC Series in Computing (Vol.\u00a033, pp. 37\u201341). EasyChair."},{"key":"10.3233\/AO-190213_ref10","unstructured":"Benzm\u00fcller, C. & Woltzenlogel Paleo, B. (2015). Higher-order modal logics: Automation and applications. In A. Paschke and W. Faber (Eds.), Reasoning Web 2015. LNCS (Vol.\u00a09203, pp. 32\u201374). Berlin, Germany: Springer. (Invited paper)."},{"issue":"2","key":"10.3233\/AO-190213_ref11","doi-asserted-by":"publisher","first-page":"135","DOI":"10.3233\/AO-180195","article-title":"Formal ontology of space, time, and physical entities in classical mechanics","volume":"13","author":"Bittner","year":"2018","journal-title":"Applied Ontology"},{"key":"10.3233\/AO-190213_ref12","unstructured":"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.\u00a04278, pp. 1626\u20131635). Berlin Heidelberg: Springer."},{"key":"10.3233\/AO-190213_ref13","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1016\/j.artmed.2006.12.005","article-title":"Logical properties of foundational relations in bio-ontologies","volume":"39","author":"Bittner","year":"2007","journal-title":"Artificial Intelligence in Medicine"},{"key":"10.3233\/AO-190213_ref15","doi-asserted-by":"crossref","unstructured":"Butterfield, J. (2007). On symplectic reduction in classical mechanics. In J. Butterfield and J. Earman (Eds.), Philosophy of Physics. Elsevier.","DOI":"10.1016\/B978-044451560-5\/50004-X"},{"key":"10.3233\/AO-190213_ref16","unstructured":"Champollion, L. & Krifka, M. (2015). Mereology. In P. Dekker and M. Aloni (Eds.), Cambridge Handbook of Formal Semantics. Cambridge University Press."},{"issue":"2","key":"10.3233\/AO-190213_ref17","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","article-title":"A formulation of the simple theory of types","volume":"5","author":"Church","year":"1940","journal-title":"The Journal of Symbolic Logic"},{"key":"10.3233\/AO-190213_ref18","unstructured":"Church, A. (1941). The Calculi of Lambda-Conversation. Princeton, NY: Princeton University Press."},{"key":"10.3233\/AO-190213_ref19","unstructured":"Copi, I. (1979). Symbolic Logic. Upper Saddle River, NJ: Prentice Hall."},{"key":"10.3233\/AO-190213_ref20","unstructured":"Einstein, A. (1951). Relativity: The Special and the General Theory. New York: Crown Publishers Inc."},{"key":"10.3233\/AO-190213_ref21","unstructured":"Foster, S., Zeyda, F. & Woodcock, J. (2015). Isabelle\/UTP: A mechanised theory engineering framework. In D. Naumann (Ed.), Unifying Theories of Programming (pp. 21\u201341). Cham: Springer."},{"key":"10.3233\/AO-190213_ref22","unstructured":"Gabbay, D.M. (2003). Many-Dimensional Modal Logics: Theory and Applications. North Holland: Elsevier."},{"issue":"3","key":"10.3233\/AO-190213_ref23","first-page":"13","article-title":"Sweetening ontologies with DOLCE","volume":"23","author":"Gangemi","year":"2003","journal-title":"AI Magazine"},{"key":"10.3233\/AO-190213_ref24","unstructured":"Haarslev, V. & M\u00f6ller, 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\u201336)."},{"key":"10.3233\/AO-190213_ref25","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-69778-0_30"},{"key":"10.3233\/AO-190213_ref26","unstructured":"Hughes, G. & Cresswell, M. (2004). A New Introduction to Modal Logic. London and New York: Routledge."},{"key":"10.3233\/AO-190213_ref27","doi-asserted-by":"publisher","DOI":"10.1145\/165180.165190"},{"key":"10.3233\/AO-190213_ref29","unstructured":"Kamm\u00fcller, F., Wenzel, M. & Paulson, L.C. (1999). Locales a sectioning concept for Isabelle. In Y. Bertot, G. Dowek, L. Th\u00e9ry, A. Hirschowitz and C. Paulin (Eds.), Theorem Proving in Higher Order Logics: 12th International Conference, TPHOLs\u2019 99, Proceedings. Nice, France, September 14\u201317, 1999. (pp. 149\u2013165). Berlin Heidelberg: Springer."},{"key":"10.3233\/AO-190213_ref30","unstructured":"Knublauch, H., Fergerson, R.W., Noy, N.F. & Musen, M.A. (2004). The prot\u00e9g\u00e9 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."},{"key":"10.3233\/AO-190213_ref31","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-011-3969-4_9"},{"key":"10.3233\/AO-190213_ref33","doi-asserted-by":"crossref","unstructured":"Loui, M.C. (1996). Computational complexity theory. ACM Computing Surveys, 28(1).","DOI":"10.1145\/234313.234337"},{"key":"10.3233\/AO-190213_ref34","unstructured":"Lowe, E.J. (2002). A Survey of Metaphysics. Oxford University Press."},{"key":"10.3233\/AO-190213_ref35","unstructured":"Milner, R., Tofte, M. & Harper, R. (1990). The Definition of Standard ML. MIT Press."},{"key":"10.3233\/AO-190213_ref37","unstructured":"Mossakowski, T., Maeder, C. & L\u00fcttich, K. (2007). The heterogeneous tool set. In O. Grumberg and M. Huth (Eds.), TACAS 2007. Lecture Notes in Computer Science (Vol.\u00a04424, pp. 519\u2013522). Springer."},{"key":"10.3233\/AO-190213_ref38","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-39185-1_15"},{"key":"10.3233\/AO-190213_ref39","unstructured":"Nipkow, T., Paulson, L.C. & Wenzel, M. (2002). Isabelle\/HOL\u00a0\u2013 a Proof Assistant for Higher-Order Logic (Vol.\u00a02283). Springer."},{"key":"10.3233\/AO-190213_ref40","unstructured":"Norton, J.D. (2012). Einstein\u2019s 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."},{"key":"10.3233\/AO-190213_ref43","unstructured":"Paulson, L.C. (1994). Isabelle: A Generic Theorem Prover. Springer."},{"issue":"1\u20132","key":"10.3233\/AO-190213_ref44","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1016\/S0004-3702(99)00002-8","article-title":"On the complexity of qualitative spatial reasoning: A maximal tractable fragment of the region connection calculus","volume":"108","author":"Renz","year":"1999","journal-title":"Artificial Intelligence"},{"key":"10.3233\/AO-190213_ref45","unstructured":"Simons, P. (1987). Parts, a Study in Ontology. Oxford: Clarendon Press."},{"key":"10.3233\/AO-190213_ref46","doi-asserted-by":"publisher","DOI":"10.1016\/j.websem.2007.03.004"},{"key":"10.3233\/AO-190213_ref47","unstructured":"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\u2013166). Oxford: Blackwell."},{"issue":"2","key":"10.3233\/AO-190213_ref49","doi-asserted-by":"publisher","first-page":"401","DOI":"10.2307\/2653492","article-title":"Fiat and Bona fide boundaries","volume":"60","author":"Smith","year":"2000","journal-title":"Philosophy and Phenomenological Research"},{"issue":"2","key":"10.3233\/AO-190213_ref50","doi-asserted-by":"publisher","first-page":"175","DOI":"10.2307\/421089","article-title":"Tarski\u2019s system of geometry","volume":"5","author":"Tarski","year":"1999","journal-title":"Bulletin of Symbolic Logic"},{"key":"10.3233\/AO-190213_ref51","unstructured":"Thompson, S. (1999). Haskell: The Craft of Functional Programming (2nd ed.). Addison-Wesley."},{"key":"10.3233\/AO-190213_ref52","unstructured":"Varzi, A. (2003). Mereology. In E.N. Zalta (Ed.), Stanford Encyclopedia of Philosophy. Stanford: CSLI (internet publication)."},{"key":"10.3233\/AO-190213_ref56","unstructured":"Wikimedia Commons (2013). File:slope field.png\u00a0\u2013 Wikimedia Commons, the free media repository. [Online; accessed 21-January-2018]."},{"key":"10.3233\/AO-190213_ref57","unstructured":"Wikimedia Commons (2015a). File:image tangent-plane.svg\u00a0\u2013 Wikimedia Commons, the free media repository. [Online; accessed 21-January-2018]."},{"key":"10.3233\/AO-190213_ref58","unstructured":"Wikimedia Commons (2015b). Two coordinate charts on a manifold. Licensed under Creative Commons Attribution-Share Alike 3.0 via Wikimedia Commons."}],"container-title":["Applied Ontology"],"original-title":[],"link":[{"URL":"https:\/\/content.iospress.com\/download?id=10.3233\/AO-190213","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,10]],"date-time":"2025-03-10T23:16:05Z","timestamp":1741648565000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/full\/10.3233\/AO-190213"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,8,19]]},"references-count":46,"journal-issue":{"issue":"3"},"URL":"https:\/\/doi.org\/10.3233\/ao-190213","relation":{},"ISSN":["1875-8533","1570-5838"],"issn-type":[{"type":"electronic","value":"1875-8533"},{"type":"print","value":"1570-5838"}],"subject":[],"published":{"date-parts":[[2019,8,19]]}}}