From: "Achim D. Brucker" <brucker@spamfence.net>
Dear all,
We proudly present our next public release for our Document Ontology
Framework (DOF) conceived as add-on of Isabelle/HOL. The installation
should work under Isabelle 2021 and TeX Live 2021 out of the box.
Homepage: https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF
Long-term Archive: https://zenodo.org/record/4625176
Best,
Achim & Burkhart
MISSION
=======
DOF permits to annotate theory-elements and terms
with structured, typed meta-data, which were used in
automatically generated antiquotations. DOF applications
are currently mostly geared (but not restricted) to document
generation processes, so mostly technical reports,
theory-documentations, and scientific papers.
The meta-data can be specified in a HOL-like syntax
via Ontologies, that were associated to appropriate
LaTeX style files. IDE Support in Isabelle/PIDE allows for
a smooth, ontology-conform editing process of texts that
contain both formal and informal content as well as
machine-checked links between them.
KEY FEATURES
=============
constructs to define text elements as INSTANCES of ontological
classes (e.g., a "requirement")
ways to annotate them with informal and formal content (e.g., a
type-checked term or a thm)
generated antiquotations referring to instances via their reference
(e.g., @{requirement <xyz>} where xyz must Indeed a defined reference
to an instance.
temporal and data constraints similar to class invariants on
meta-data
navigation support via PIDE in documents and ontologies
Last updated: Jan 04 2025 at 20:18 UTC