| dc.contributor.author | Brucker, AD | |
| dc.contributor.author | Méric, N | |
| dc.contributor.author | Wolff, B | |
| dc.date.accessioned | 2024-05-28T12:48:03Z | |
| dc.date.issued | 2024-04-26 | |
| dc.date.updated | 2024-05-26T08:44:42Z | |
| dc.description.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. | en_GB |
| dc.description.sponsorship | IRT SystemX, Paris-Saclay, France | en_GB |
| dc.identifier.citation | Published online 26 April 2024 | en_GB |
| dc.identifier.uri | http://hdl.handle.net/10871/136049 | |
| dc.identifier | ORCID: 0000-0002-6355-1200 (Brucker, Achim D) | |
| dc.language.iso | en | en_GB |
| dc.publisher | AFP | en_GB |
| dc.relation.url | https://www.isa-afp.org/entries/Isabelle_DOF.html | en_GB |
| dc.rights | © 2019–2024 University of Exeter, UK
2018–2024 Université Paris-Saclay, France
2018–2019 The University of Sheffield, UK
Redistribution and use in source and binary forms, with or without modification, are permitted pro vided that the following conditions are met:
• Redistributions of source code must retain the above copyright notice, this list of conditions
and the following disclaimer.
• Redistributions in binary form must reproduce the above copyright notice, this list of conditions
and the following disclaimer in the documentation and/or other materials provided with the
distribution.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS “AS
IS” AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO,
THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIB UTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUB STITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTER RUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CON TRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING
IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY
OF SUCH DAMAGE.
SPDX-License-Identifier: BSD-2-Clause | en_GB |
| dc.title | Isabelle/DOF. User and Implementation Manual (2024) | en_GB |
| dc.type | Article | en_GB |
| dc.date.available | 2024-05-28T12:48:03Z | |
| dc.identifier.issn | 2150-914X | |
| dc.description | This is the final version. Available from AFP via the link in this record | en_GB |
| dc.identifier.journal | Archive of Formal Proofs | en_GB |
| dc.rights.uri | https://www.isa-afp.org/LICENSE | en_GB |
| rioxxterms.version | VoR | en_GB |
| rioxxterms.licenseref.startdate | 2024-04-26 | |
| rioxxterms.type | Journal Article/Review | en_GB |
| refterms.dateFCD | 2024-05-28T12:45:34Z | |
| refterms.versionFCD | VoR | |
| refterms.dateFOA | 2024-05-28T12:48:06Z | |
| refterms.panel | B | en_GB |
