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

New Release - Isabelle/DOF 1.0.0

We are proud to announce the first public release of Isabelle/DOF. Isabelle/DOF is a Document Ontology Framework (DOF) allowing annotating text elements in formal developments with structured, typed meta-information. Developers can define this meta-information according to their needs, e.g., to enable semantic queries (in the sense of semantic web), tool interaction, or document generation.

Currently, Isabelle/DOF focuses on the generation of documents with formal and semi-formal or informal content. While Isabelle/DOF is developed on top of Isabelle/HOL, its users are not necessarily Isabelle users: Isabelle/DOF aims at authors of any type of documents involving formal content or formal structure. Possible application areas are, e.g., mathematical papers, or documents with certification processes.

Isabelle/DOF can be downloaded from its website: https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF/ Alternatively, a Docker image is available that allows to directly start Isabelle/DOF (this requires a host operating system with an X-Sever):

docker run -ti --rm -e DISPLAY=$DISPLAY -v /tmp/.X11-unix:/tmp/.X11-unix \
           logicalhacking/isabelle_dof-1.0.0_isabelle2019 isabelle jedit

As the Isabelle/DOF installation requires applying a small patch to Isabelle itself, the Docker image is helpful for users that want to avoid modifying Isabelle itself.

The Isabelle/DOF distribution contains the Isabelle/DOF: User and Implementation Manual and the system is also described in [1] and [2]. The manual and [2] are written using Isabelle/DOF.

Supplementary Material

References

1. Brucker, A. D. and Wolff, B. “Isabelle/DOF: Design and ImplementationSoftware engineering and formal methods (SEFM) (2019): doi:10.1007/978-3-030-30446-1_15, URL: http://www.brucker.ch/bibliography/abstract/brucker.ea-isabelledof-2019

2. Brucker, A. D., Ait-Sadoune, I., Crisafulli, P., and Wolff, B. “Using the Isabelle Ontology Framework: Linking the Formal with the InformalConference on intelligent computer mathematics (CICM) (2018): doi:10.1007/978-3-319-96812-4_3, URL: http://www.brucker.ch/bibliography/abstract/brucker.ea-isabelle-ontologies-2018