Isabelle/DOF. User and Implementation Manual (2024)

Abstract

This manual describes Isabelle/DOF as available in the Archive of Formal Proofs (AFP). The latest development version as well as releases that can be installed as Isabelle component are available at https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF/. Isabelle/DOF provides an implementation of a document ontology framework on top of Isabelle/HOL. The framework allows both for defining ontologies and enforcing them during document development and document evolution. Isabelle/DOF targets use-cases such as mathematical texts referring to a theory development or technical reports requiring a particular structure. The documentation generation features are sufficiently powerful to typeset the most common cases without using LaTeX. Isabelle/DOF is integrated into Isabelle’s IDE, which allows for smooth ontology development as well as immediate ontological conformance-checks during the editing of a document. Its checking facilities leverage the collaborative development of documents required to be consistent with an underlying ontological structure. This entry provides a user-manual with in-depth presentation of the design concepts of Isabelle/DOF’s Ontology Definition Language (ODL) and describe comprehensively its major commands. Many examples show typical best-practice applications of the system.