On the computational realization of formal ontologies: Formalizing an ontology of instantiation in spacetime using Isabelle/HOL as a case study

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.