Abstract
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.
License
Topics
Related publications
- Brucker, A. D., Ait-Sadoune, I., Crisafulli, P., & Wolff, B. (2018). Using the Isabelle Ontology Framework. Intelligent Computer Mathematics, 23–38. https://doi.org/10.1007/978-3-319-96812-4_3
- Brucker, A. D., & Wolff, B. (2019). Isabelle/DOF: Design and Implementation. Software Engineering and Formal Methods, 275–292. https://doi.org/10.1007/978-3-030-30446-1_15
- Brucker, A. D., & Wolff, B. (2019). Using Ontologies in Formal Developments Targeting Certification. Integrated Formal Methods, 65–82. https://doi.org/10.1007/978-3-030-34968-4_4
Session Isabelle_DOF
- RegExpInterface
- Isa_DOF
- Isa_COL
- scholarly_paper
- technical_report
- ontologies
- M_00_Frontmatter
- M_01_Introduction
- M_02_Background
- M_03_GuidedTour
- M_04_Document_Ontology
- M_05_Proofs_Ontologies
- M_06_RefMan
- M_07_Implementation
- Isabelle_DOF_Manual