nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Ensured that DOF is already introduced in the introduction.

This commit is contained in:
Achim D. Brucker 2019-08-02 16:24:37 +01:00
parent 5668e3c56d
commit 95dc57891b
1 changed files with 9 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy
View File

@ -29,13 +29,15 @@ In general, an ontology is a formal explicit description of \<^emph>\<open>conce
as \<^emph>\<open>links\<close> between them. A particular link between concepts is the \<^emph>\<open>is-a\<close> 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>\<open>model\<close> typed ontologies and to
\<^emph>\<open>enforce\<close> 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>\<open>conform\<close> to a particular ontology---\isadof is designed
to give fast user-feedback \<^emph>\<open>during the capture of content\<close>. This is particularly valuable in case
of document evolution, where the \<^emph>\<open>coherence\<close> 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>\<open>model\<close> typed ontologies and to \<^emph>\<open>enforce\<close> 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>\<open>conform\<close> to a particular ontology---\isadof is designed to give fast user-feedback \<^emph>\<open>during the
capture of content\<close>. This is particularly valuable in case of document evolution, where the
\<^emph>\<open>coherence\<close> between the formal and the informal parts of the content can be mechanically checked.
To avoid any misunderstanding: \isadof is \<^emph>\<open>not a theory in HOL\<close> on ontologies and operations to
track and trace links in texts, it is an \<^emph>\<open>environment to write structured text\<close> which