### 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

BSD License

### Topics

- Computer science/Semantics and reasoning

### 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. Lecture Notes in Computer Science, 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

### Depends on

- Functional Automata
- Regular Sets and Expressions

## Cite

×

Isabelle_DOF-AFP

    @article{Isabelle_DOF-AFP,
      author  = {Achim D. Brucker and Nicolas Méric and Burkhart Wolff},
      title   = {Isabelle/DOF},
      journal = {Archive of Formal Proofs},
      month   = {April},
      year    = {2024},
      note    = {\url{https://isa-afp.org/entries/Isabelle_DOF.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest