Show simple item record

dc.contributor.authorBrucker, AD
dc.contributor.authorWolff, B
dc.date.accessioned2019-08-20T12:01:37Z
dc.date.issued2019-08-18
dc.description.abstractIsabelle/DOF provides an implementation of DOF on top of Isabelle/HOL. DOF itself is a novel framework 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. A major application of DOF is the integrated development of formal certification documents (e.g., for Common Criteria or CENELEC 50128) that require consistency across both formal and informal arguments. Isabelle/DOF is integrated into Isabelle’s IDE, which allows for smooth ontology development as well as immediate ontological feedback during the editing of a document. Its checking facilities leverage the collaborative development of documents required to be consistent with an underlying ontological structure. In this user-manual, we give an in-depth presentation of the design concepts of DOF’s Ontology Definition Language (ODL) and describe comprehensively its major commands. Many examples show typical best-practice applications of the system. Isabelle/DOF is the first ontology language supporting machine-checked links between the formal and informal parts in an LCF-style interactive theorem proving environment.en_GB
dc.description.sponsorshipIRT SystemXen_GB
dc.identifier.doi10.5281/zenodo.3370483
dc.identifier.urihttp://hdl.handle.net/10871/38402
dc.language.isoenen_GB
dc.publisherUniversity of Exeter / Université Paris-Saclay / University of Sheffielden_GB
dc.rights© 2019 University of Exeter / Université Paris-Saclay / University of Sheffielden_GB
dc.subjectOntologyen_GB
dc.subjectOntological Modelingen_GB
dc.subjectDocument Managementen_GB
dc.subjectFormal Document Developmenten_GB
dc.subjectDocument Authoringen_GB
dc.subjectIsabelle/DOFen_GB
dc.titleIsabelle/DOF. User and Implementation Manualen_GB
dc.typeOtheren_GB
dc.date.available2019-08-18en_GB
dc.date.available2019-08-20T12:01:37Z
pubs.notesNot knownen_GB
pubs.version1.0.0/Isabelle2019en_GB
dc.descriptionThe software for which this is the manual is available via the DOI in this recorden_GB
dc.rights.urihttp://www.rioxx.net/licenses/all-rights-reserveden_GB
rioxxterms.versionVoRen_GB
rioxxterms.licenseref.startdate2019-08-18
rioxxterms.typeOtheren_GB
refterms.dateFCD2019-08-20T11:59:32Z
refterms.versionFCDVoR
refterms.dateFOA2019-08-20T12:01:39Z


Files in this item

This item appears in the following Collection(s)

Show simple item record