forked from Isabelle_DOF/Isabelle_DOF
Reworked textually abstract, intro, background. Eliminate \emph
This commit is contained in:
parent
8002ec31bb
commit
f239b36b49
|
@ -1,7 +1,7 @@
|
||||||
(*************************************************************************
|
(*************************************************************************
|
||||||
* Copyright (C)
|
* Copyright (C)
|
||||||
* 2019 The University of Exeter
|
* 2019-20 The University of Exeter
|
||||||
* 2018-2019 The University of Paris-Saclay
|
* 2018-2020 The University of Paris-Saclay
|
||||||
* 2018 The University of Sheffield
|
* 2018 The University of Sheffield
|
||||||
*
|
*
|
||||||
* License:
|
* License:
|
||||||
|
@ -54,10 +54,13 @@ text*[abs::abstract,
|
||||||
In this user-manual, we give an in-depth presentation of the design
|
In this user-manual, we give an in-depth presentation of the design
|
||||||
concepts of \dof's Ontology Definition Language (ODL) and describe
|
concepts of \dof's Ontology Definition Language (ODL) and describe
|
||||||
comprehensively its major commands. Many examples show typical best-practice
|
comprehensively its major commands. Many examples show typical best-practice
|
||||||
applications of the system. \isadof is the
|
applications of the system.
|
||||||
first ontology language supporting machine-checked
|
|
||||||
links between the formal and informal parts in an LCF-style
|
It is an unique feature of \isadof that ontologies may be used to control
|
||||||
interactive theorem proving environment.
|
the link between formal and informal content in documents in a machine
|
||||||
|
checked way. These links can connect both text elements as well as formal
|
||||||
|
modelling elements such as terms, definitions, code and logical formulas,
|
||||||
|
alltogether *\<open>integrated\<close> in a state-of-the-art interactive theorem prover.
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
(*<*)
|
(*<*)
|
||||||
|
|
|
@ -1,7 +1,7 @@
|
||||||
(*************************************************************************
|
(*************************************************************************
|
||||||
* Copyright (C)
|
* Copyright (C)
|
||||||
* 2019 The University of Exeter
|
* 2019-2020 The University of Exeter
|
||||||
* 2018-2019 The University of Paris-Saclay
|
* 2018-2020 The University of Paris-Saclay
|
||||||
* 2018 The University of Sheffield
|
* 2018 The University of Sheffield
|
||||||
*
|
*
|
||||||
* License:
|
* License:
|
||||||
|
@ -33,8 +33,8 @@ have to follow a structure. In practice, large groups of developers have to pro
|
||||||
set of documents where the consistency is notoriously difficult to maintain. In particular,
|
set of documents where the consistency is notoriously difficult to maintain. In particular,
|
||||||
certifications are centered around the \<^emph>\<open>traceability\<close> of requirements throughout the entire
|
certifications are centered around the \<^emph>\<open>traceability\<close> of requirements throughout the entire
|
||||||
set of documents. While technical solutions for the traceability problem exists (most notably:
|
set of documents. While technical solutions for the traceability problem exists (most notably:
|
||||||
DOORS~\cite{ibm:doors:2019}), they are weak in the treatment of formal entities (such as formulas and their
|
DOORS~\cite{ibm:doors:2019}), they are weak in the treatment of formal entities (such as formulas
|
||||||
logical contexts).
|
and their logical contexts).
|
||||||
|
|
||||||
Further applications are the domain-specific discourse in juridical texts or medical reports.
|
Further applications are the domain-specific discourse in juridical texts or medical reports.
|
||||||
In general, an ontology is a formal explicit description of \<^emph>\<open>concepts\<close> in a domain of discourse
|
In general, an ontology is a formal explicit description of \<^emph>\<open>concepts\<close> in a domain of discourse
|
||||||
|
@ -43,11 +43,12 @@ as \<^emph>\<open>links\<close> between them. A particular link between concepts
|
||||||
the instances of a subclass to be instances of the super-class.
|
the instances of a subclass to be instances of the super-class.
|
||||||
|
|
||||||
To adress this challenge, we present the Document Ontology Framework (\dof) and an
|
To adress this challenge, we present the Document Ontology Framework (\dof) and an
|
||||||
implementation of DOF called \isadof. \dof is designed for building scalable and user-friendly
|
implementation of \dof called \isadof. \dof is designed for building scalable and user-friendly
|
||||||
tools on top of interactive theorem provers. \isadof is a novel framework, implemented as extension of
|
tools on top of interactive theorem provers. \isadof is an instance of this novel framework,
|
||||||
Isabelle/HOL, to \<^emph>\<open>model\<close> typed ontologies and to \<^emph>\<open>enforce\<close> them during document evolution. Based
|
implemented as extension of Isabelle/HOL, to \<^emph>\<open>model\<close> typed ontologies and to \<^emph>\<open>enforce\<close> them
|
||||||
on Isabelle's infrastructures, ontologies may refer to types, terms, proven theorems, code, or
|
during document evolution. Based on Isabelle's infrastructures, ontologies may refer to types,
|
||||||
established assertions. Based on a novel adaption of the Isabelle IDE, a document is checked to be
|
terms, proven theorems, code, or established assertions. Based on a novel adaption of the Isabelle
|
||||||
|
IDE (called PIDE, @{cite "wenzel:asynchronous:2014"}), 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
|
\<^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
|
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.
|
\<^emph>\<open>coherence\<close> between the formal and the informal parts of the content can be mechanically checked.
|
||||||
|
|
|
@ -91,9 +91,9 @@ text\<open>
|
||||||
separate commands from each other.
|
separate commands from each other.
|
||||||
|
|
||||||
We distinguish fundamentally two different syntactic levels:
|
We distinguish fundamentally two different syntactic levels:
|
||||||
\<^item> the \emph{outer-syntax}\bindex{syntax!outer}\index{outer syntax|see {syntax, outer}} (\ie, the
|
\<^item> the *\<open>outer-syntax\<close>\bindex{syntax!outer}\index{outer syntax|see {syntax, outer}} (\ie, the
|
||||||
syntax for commands) is processed by a lexer-library and parser combinators built on top, and
|
syntax for commands) is processed by a lexer-library and parser combinators built on top, and
|
||||||
\<^item> the \emph{inner-syntax}\bindex{syntax!inner}\index{inner syntax|see {syntax, inner}} (\ie, the
|
\<^item> the *\<open>inner-syntax\<close>\bindex{syntax!inner}\index{inner syntax|see {syntax, inner}} (\ie, the
|
||||||
syntax for \inlineisar|\<lambda>|-terms in HOL) with its own parametric polymorphism type
|
syntax for \inlineisar|\<lambda>|-terms in HOL) with its own parametric polymorphism type
|
||||||
checking.
|
checking.
|
||||||
|
|
||||||
|
@ -108,14 +108,14 @@ text\<open>
|
||||||
\end{isar}
|
\end{isar}
|
||||||
This will type-set the corresponding text in, for example, a PDF document. However, this
|
This will type-set the corresponding text in, for example, a PDF document. However, this
|
||||||
translation is not necessarily one-to-one: text elements can be enriched by formal, \ie,
|
translation is not necessarily one-to-one: text elements can be enriched by formal, \ie,
|
||||||
machine-checked content via \emph{semantic macros}, called antiquotations\bindex{antiquotation}:
|
machine-checked content via *\<open>semantic macros\<close>, called antiquotations\bindex{antiquotation}:
|
||||||
\begin{isar}
|
\begin{isar}
|
||||||
text\<Open>According to the reflexivity axiom <@>{thm refl}, we obtain in \<Gamma>
|
text\<Open>According to the *\<Open>reflexivity\<Close> axiom <@>{thm refl}, we obtain in \<Gamma>
|
||||||
for <@>{term "fac 5"} the result <@>{value "fac 5"}.\<Close>
|
for <@>{term "fac 5"} the result <@>{value "fac 5"}.\<Close>
|
||||||
\end{isar}
|
\end{isar}
|
||||||
which is represented in the final document (\eg, a PDF) by:
|
which is represented in the final document (\eg, a PDF) by:
|
||||||
\begin{out}
|
\begin{out}
|
||||||
According to the reflexivity axiom $\mathrm{x = x}$, we obtain in $\Gamma$ for $\operatorname{fac} \text{\textrm{5}}$ the result $\text{\textrm{120}}$.
|
According to the \emph{reflexivity} axiom $\mathrm{x = x}$, we obtain in $\Gamma$ for $\operatorname{fac} \text{\textrm{5}}$ the result $\text{\textrm{120}}$.
|
||||||
\end{out}
|
\end{out}
|
||||||
Semantic macros are partial functions of type \inlineisar+\<theta> \<rightarrow> text+; since they can use the
|
Semantic macros are partial functions of type \inlineisar+\<theta> \<rightarrow> text+; since they can use the
|
||||||
system state, they can perform all sorts of specific checks or evaluations (type-checks,
|
system state, they can perform all sorts of specific checks or evaluations (type-checks,
|
||||||
|
|
Reference in New Issue