Isabelle/DOF is a novel Document Ontology Framework on top of Isabelle. Isabelle/DOF allows for both conventional typesetting and formal development.
Isabelle/DOF has two major prerequisites:
Isabelle/DOF is available as part of the Archive of Formal Proofs (AFP). This is the most convenient way to install Isabelle/DOF for the latest official release of Isabelle.
Installation from the Archive of Formal Proofs (AFP)Isabelle/DOF is available in the AFP. Hence, for using Isabelle/DOF with the latest official released version of Isabelle, please download the Isabelle distribution for your operating system from the Isabelle website. Furthermore, please install the AFP following the instructions given at https://www.isa-afp.org/help.html.
Isabelle/DOF is provided as one AFP entry:
Add-ons to Isabelle/DOF, in particular, additional ontologies, document templates, and examples, are provided on Zenodo.
Installation of the Development Version (Git Repository)The development version of Isabelle/DOF that is available in this Git repository provides, over the AFP version, additional ontologies, document templates, and examples that might not yet “ready for general use”. Furthermore, as it is provided as an Isabelle component, it can also provide additional tools that cannot be distributed via the AFP. As this repository provides a (potentially) updated version of Isabelle/DOF, it conflicts with a complete installation of the AFP. For more details on installing the development version, please consult the README_DEVELOPMENT.md file.
After installing the prerequisites, change into the directory containing Isabelle/DOF (this should be the directory containing this README.md file) and execute the following command for building the standard sessions of Isabelle/DOF:
foo@bar:~$ isabelle build -D . -x Isabelle_DOF-Proofs -x HOL-Proofs
This will compile Isabelle/DOF and run the example suite.
For building the session Isabelle_DOF-Proofs, the timeout might need to increased to avoid timeouts during building the dependencies:
foo@bar:~$ isabelle build -d . -o 'timeout_scale=2' Isabelle_DOF-Proofs
In the following, we assume that you installed Isabelle/DOF either from the AFP (adding the AFP as a component to your Isabelle system) with the add-ons available on Zenodo (or from the Git repository of Isabelle/DOF).
Assuming that your current directory contains the example academic paper in the subdirectory Isabelle_DOF-Example-I/, you can open it similar to any standard Isabelle theory:
isabelle jedit -l Isabelle_DOF Isabelle_DOF-Example-I/IsaDofApplications.thy
This will open an example of a scientific paper using the pre-compiled session Isabelle_DOF, i.e., you will not be able to edit the default ontologies defined in the Isabelle_DOF session. If you want to edit the ontology definition, just open the theory file with the session Functional-Automata:
isabelle jedit -l Functional-Automata Isabelle_DOF-Example-I/IsaDofApplications.thy
While this gives you more flexibility, it might "clutter" your editing experience, as a lot of internal theories are loaded into Isabelle's editor.
The main branch of this repository is developed using the latest official release of Isabelle. This is also the main development branch. In addition, he [isabelle_nightly](https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF/src/branch/isabelle_nightly) branch is used for testing Isabelle/DOF with the latest development version of Isabelle.
This repository is structured into several Isabelle sessions, each of which is stored in a subdirectory:
Isabelle_DOF session. Furthermore, this session is currently under consideration for a submission to the AFP.Isabelle_DOF-Ontologies session.Since Isabelle 2024, Isabelle/DOF synchronises its releases with the releases of Isabelle. The core of Isabelle/DOF is part of the Archive of Formal Proofs and several add-on packages are released on Zenodo.
Older releases are available here.
Main contacts:
This project is licensed under a 2-clause BSD license.
SPDX-License-Identifier: BSD-2-Clause
Achim D. Brucker, Idir Aït-Sadoune, Nicolas Méric, Burkhart Wolff: Parametric ontologies in formal software engineering. Sci. Comput. Program. 241: 103231 (2025). do:10.1016/j.scico.2024.103231
Nicolas Méric: An Ontology Framework for Formal Libraries: Doctoral Thesis at the University Pris-Saclay. (Conception et Implémentation d'un Environnement d'Ontologie pour des Bibliothèques Formelles). University of Paris-Saclay, France, 2024. https://tel.archives-ouvertes.fr/tel-04870527
Achim D. Brucker, Idir Aït-Sadoune, Nicolas Méric, Burkhart Wolff: Using Deep Ontologies in Formal Software Engineering. ABZ 2023: 15-32. doi:10.1007/978-3-031-33163-3_2
Achim D. Brucker, Idir Ait-Sadoune, Paolo Crisafulli, and Burkhart Wolff. Using The Isabelle Ontology Framework: Linking the Formal with the Informal. In Conference on Intelligent Computer Mathematics (CICM). Lecture Notes in Computer Science (11006), Springer-Verlag, 2018. doi:10.1007/978-3-319-96812-4_3.
Achim D. Brucker and Burkhart Wolff. Isabelle/DOF: Design and Implementation. In Software Engineering and Formal Methods (SEFM). Lecture Notes in Computer Science (11724), Springer-Verlag, 2019. doi:10.1007/978-3-030-30446-1_15.
Achim D. Brucker, Burkhart Wolff. Using Ontologies in Formal Developments Targeting Certification. In Integrated Formal Methods (IFM). Lecture Notes in Computer Science (11918). Springer-Verlag 2019. doi:10.1007/978-3-030-34968-4_4
Sergio Bezzecchi, Paolo Crisafulli, Charlotte Pichot, and Burkhart Wolff. Making Agile Development Processes fit for V-style Certification Procedures.. In ERTS 2018. https://hal.archives-ouvertes.fr/hal-01702815
The upstream git repository, i.e., the single source of truth, for this project is hosted at https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF.
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4