From 3eba90f97827b4fd57fb3a7083a7b5e08dbd980e Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Tue, 30 Jul 2019 22:57:22 +0100 Subject: [PATCH] Revised abstract. --- .../Isabelle_DOF-Manual/00_Frontmatter.thy | 37 ++++++++++--------- 1 file changed, 19 insertions(+), 18 deletions(-) diff --git a/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy b/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy index 13322e13..4ac5e3ef 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy @@ -18,28 +18,29 @@ text*[bu::author, email = "\wolff@lri.fr\", affiliation = "\Université Paris-Saclay, LRI, Paris, France\"]\Burkhart Wolff\ - text*[abs::abstract, - keywordlist="[''Ontology'',''Ontological Modeling'',''Isabelle/DOF'']"]\ -While Isabelle is mostly known as part of Isabelle/HOL (an interactive -theorem prover), it actually provides a framework for developing a wide -spectrum of applications. A particular strength -of the Isabelle framework is the combination of text editing, formal verification, -and code generation. + keywordlist="[''Ontology'', ''Ontological Modeling'', ''Document Management'', + ''Formal Document Development'', ''Document Authoring'', ''Isabelle/DOF'']"] +\ \isadof provides an implementation of \dof on top of Isabelle/HOL. + \dof itself is a novel framework for \<^emph>\defining\ ontologies + and \<^emph>\enforcing\ them during document development and document + evolution. A major goal of \dof is the integrated development of + formal certification documents (\eg, for Common Criteria or CENELEC + 50128) that require consistency across both formal and informal + arguments. -Up to now, Isabelle's document preparation system lacks a mechanism -for ensuring the structure of different document types (as, e.g., -required in certification processes) in general and, in particular, -a \<^emph>\systematic\ mechanism for linking informal and formal parts of a document. - -In this paper, we present \isadof, a novel Document Ontology Framework -on top of Isabelle. \isadof allows for conventional typesetting -\<^emph>\as well\ as formal development. We show how to model document - ontologies inside \isadof, how to use the resulting meta-information -for enforcing a certain document structure, and discuss ontology-specific IDE support. + \isadof is integrated into Isabelle's IDE, which + allows for smooth ontology development as well as immediate + ontological feedback during the editing of a document. + + In this paper, we give an in-depth presentation of the design + concepts of \dof's Ontology Definition Language (ODL) and key + aspects of the technology of its implementation. \isadof is the + first ontology language supporting machine-checked + links between the formal and informal parts in an LCF-style + interactive theorem proving environment. \ - (*<*) end (*>*)