From 95dc57891b805351c1c5546849b6f0097e459ab0 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Fri, 2 Aug 2019 16:24:37 +0100 Subject: [PATCH] Ensured that DOF is already introduced in the introduction. --- .../Isabelle_DOF-Manual/01_Introduction.thy | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy b/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy index 85e8d937..bb25c7b3 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy @@ -29,13 +29,15 @@ In general, an ontology is a formal explicit description of \<^emph>\conce as \<^emph>\links\ between them. A particular link between concepts is the \<^emph>\is-a\ relation declaring the instances of a subclass to be instances of the super-class. -\isadof is a novel framework, extending of Isabelle/HOL, to \<^emph>\model\ typed ontologies and to -\<^emph>\enforce\ them during document evolution. Based on Isabelle infrastructures, ontologies may refer -to types, terms, proven theorems, code, or established assertions. Based on a novel adaption of the -Isabelle IDE, a document is checked to be \<^emph>\conform\ to a particular ontology---\isadof is designed -to give fast user-feedback \<^emph>\during the capture of content\. This is particularly valuable in case -of document evolution, where the \<^emph>\coherence\ between the formal and the informal parts of the -content can be mechanically checked. +To adress this challenge, we present developed the Document Ontology Framework (\dof). \dof is +designed for building scalable and user-friendly tools on top of interactive theorem provers, +and an implementation of DOF called \isadof. \isadof is a novel framework, extending of +Isabelle/HOL, to \<^emph>\model\ typed ontologies and to \<^emph>\enforce\ them during document evolution. Based +on Isabelle infrastructures, ontologies may refer to types, terms, proven theorems, code, or +established assertions. Based on a novel adaption of the Isabelle IDE, a document is checked to be +\<^emph>\conform\ to a particular ontology---\isadof is designed to give fast user-feedback \<^emph>\during the +capture of content\. This is particularly valuable in case of document evolution, where the +\<^emph>\coherence\ between the formal and the informal parts of the content can be mechanically checked. To avoid any misunderstanding: \isadof is \<^emph>\not a theory in HOL\ on ontologies and operations to track and trace links in texts, it is an \<^emph>\environment to write structured text\ which