Parametric Ontologies in Software Engineering
The linking of formal and informal information is perhaps the most pervasive challenge in the digitization of modern society. Extracting knowledge from reasonably well-structured “raw”-texts is a crucial prerequisite for any form of advanced search, classification, “semantic” validation and “semantic” merge technology. This challenge incites numerous research efforts summarized under the labels “semantic web” or “data mining”. A key role in structuring this linking is played by ontologies (also called “vocabulary” in semantic web communities), i.e., a machine-readable form of the structure of documents and the document discourse.
Such ontologies can be used for scientific discourse underlying scholarly articles, the conversion, and integration of semiformal content, for advanced semantic search in mathematical libraries or documentation in various domains. In other words, ontologies generate the meta-data necessary to annotate raw text allowing their “deeper analysis”, in particular inside mathematical formulas or equivalent formal content such as programs or UML-models.
To support such scenarios, we developed Isabelle/DOF, an ontology framework on top of Isabelle/HOL. It allows for the formal development of ontologies and continuous conformity-checking of integrated documents, including the tracing of typed meta-data of documents. Isabelle/DOF deeply integrates into the Isabelle/HOL ecosystem, allowing to write documents containing (informal) text, executable code, (formal and semiformal) definitions, and proofs. Users of Isabelle/DOF can either use HOL or one of the many formal methods that have been embedded into Isabelle/HOL to express formal parts of their documents.
In our most recent journal paper [1], which supersedes [2], we describe in detail, how we extended Isabelle/DOF to support parametric ontological classes.