Isabelle/DOF. User and Implementation Manual

Abstract

Isabelle/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.