Email Gateway (Aug 22 2022 at 20:25): Email Gateway (Aug 22 2022 at 20:25):From: "Achim D. Brucker" <brucker@spamfence.net>
We happily announce our 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. The system is implemented
to allow fast user-feedback in Isabelle/PIDE.
Still, the intended users are not necessarily Isabelle user, the
system is also aimed at authors of any type of documents involving
formal content and formal structure. Possible application areas are,
e.g., mathematical papers, or documents with certification
processes. Isabelle/DOF has already been used for writing 5 papers and
3 technical reports with several co-authors having either little or no
prior knowledge of Isabelle.
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 a manual (written in
Isabelle/DOF) [1] explaining its use and implementation. Moreover,
Isabelle/DOF is described in the following two papers:
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),
LNCS 11006. Springer-Verlag, 2018.
doi:10.1007/978-3-319-96812-4_3.
This paper has been written in Isabelle/DOF and its sources are
part of the Isabelle/DOF distribution.
A.D. Brucker and B. Wolff. Isabelle/DOF: Design and implementation.
In P.C. Ölveczky and G. Salaün, editors, Software Engineering and
Formal Methods (SEFM), LNCS 11724. Springer-Verlag, 2019.
doi:10.1007/978-3-030-30446-1_15.
Another notable document that is part of the Isabelle/DOF distribution
(in the folder "examples/technical_report/TR_my_commented_isabelle" or [2]
in the repository) is the "Isabelle Programming Manual", authored by
Burkhart, that is also written and maintained in Isabelle/DOF.
Enjoy !
Achim and Burkhart
[1] https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.0.0_Isabelle2019.pdf
[2] https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF/src/branch/master/examples/technical_report/TR_my_commented_isabelle
Last updated: Apr 24 2024 at 20:16 UTC