Posted on by Achim D. Brucker, licensed under CC BY-ND 4.0.

Ontologies in Isabelle/HOL?

Mentioning ontologies and Isabelle/HOL in one sentence, might sound weird for man of us. While both are somehow used for writing formal documents, the degree of formalization is, at least at the first glance, very much different.

We asked ourselves if it is possible to integrate ontologies into Isabelle, as the current document preparation system of Isabelle lacks a mechanism for ensuring the structure of different document types (as, e.g., required in certification processes) in general and, in particular, mechanism for linking informal and formal parts of a document.

The result of this work, is Isabelle/DOF, a Document Ontology Framework on top of Isabelle. Isabelle/DOF allows for both conventional typesetting and formal (proof) development.

Isabelle/DOF allows for define ontologies within Isabelle. The ontologies are deeply integrated into the Isabelle system in general and the document preparation in particular. Thus, ontological constraints defined in an ontology are checked (while writing documents) to ensure that also the semi-formal parts of a document adhere to a certain structure and, e.g., that all links and references are defined.

More details about the initial details of Isabelle/DOF can be found in our CICM paper [1]. Isabelle/DOF is licensed under a 2-clause BSD license and available in a git repository.


A. D. Brucker, I. Ait-Sadoune, P. Crisafulli, and B. Wolff, “Using the Isabelle ontology framework: Linking the formal with the informal,” in Conference on intelligent computer mathematics (CICM), Heidelberg: Springer-Verlag, 2018. doi: 10.1007/978-3-319-96812-4_3.

Welcome to the blog of the Software Assurance & Security Research Team at the University of Exeter. We blog regularly news, tips & tricks, as well as fun facts about software assurance, reliability, security, testing, verification, hacking, and logic.

You can also follow us on Twitter: @logicalhacking.




academia ai android apidesign appsec bitcoin blockchain bpmn browser browserextensions browsersecurity bug certification chrome composition cordova dast devops devsecops dom dsbd efsm epsrc event extensions fixeffort floss formaldocument formalmethods funding hol-ocl hol-testgen humanfactor hybridapps iast industry internetofthings iot isabelle/hol isabelledof isadof latex logic maintance malicous mbst mobile mobile apps modelinference modeling monads monitoring msc ocl ontology opensource owasp patches pet phd phdlife phishing policy protocols publishing reliability research safelinks safety sap sast sdlc secdevops secureprogramming security securityengineering securitytesting semantics servicecomposition skills smartcontract smartthings softwareeinginering softwaresecurity softwaresupplychain solidity staff&positions statemachine studentproject tcb test&proof testing tips&tricks tools transport tuos uk uoe upgrade usability verification vulnerabilities vulnerableapplication webinar websecurity


blog whole site