Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

polished intro

This commit is contained in:
Burkhart Wolff 2022-01-30 13:47:18 +01:00
parent c5cdf5f826
commit b35c774d27
1 changed files with 63 additions and 57 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

120
examples/scholarly_paper/2021-ITP-PMTI/paper.thy
View File

@ -36,14 +36,18 @@ abstract*[abs, keywordlist="[\<open>Ontologies\<close>,\<open>Formal Documents\<
Thus, \<^dof> is designed to annotate and interact with typed meta-data
within formal developments in Isabelle.
While prior versions of \<^dof> provided already a mechanism to check ontological \<^emph>\<open>rules\<close>
(in OWL terminology) or \<^emph>\<open>class invariants\<close> (in UML/OCL terminology) via hand-written SML test-code,
we provide in this paper a novel mechanism to specify \<^emph>\<open>invariants\<close> in \<^hol> via a reflection
mechanism. This allows for both efficient run-time checking of abstract properties of formal
% While prior versions of \<^dof> provided already a mechanism to check ontological \<^emph>\<open>rules\<close>
% (in OWL terminology) or \<^emph>\<open>class invariants\<close> (in UML/OCL terminology) via hand-written SML test-code,
% we provide in this paper a novel mechanism to specify \<^emph>\<open>invariants\<close> in \<^hol> via a reflection
% mechanism.
In this paper we extend \<^dof> with \<^emph>\<open>invariants\<close> via a reflection mechanism,
which serve as equivalent to the concept of ontological \<^emph>\<open>rules\<close> (in OWL terminology) or
\<^emph>\<open>class invariants\<close> (in UML/OCL terminology).
This allows for both efficient run-time checking of abstract properties of formal
content \<^bold>\<open>as well as\<close> formal proofs that establish mappings between different ontologies in
general and specific ontology instances in concrete cases.
With this feature widely called \<^emph>\<open>ontology mapping\<close> in the literature, our framework paves the
way for a deeper integration of ontological information in
way for a deeper integration of ontological information in, for example,
the articles of the Archive of Formal Proofs.
\<close>
@ -58,19 +62,20 @@ Formal Proofs @{cite "AFP-ref22"}, which passed the impressive numbers of 650 ar
written by 420 authors at the beginning of 2022. Still, while the problem of logical consistency
even under system-changes and pervasive theory evolution is technically solved via continuous
proof-checking, the problem of knowledge retrieval and of linking semi-formal explanations to
definitions and proofs remains largely unresolved.
definitions and proofs remains largely open.
The \<^emph>\<open>knowledge\<close> problem of the increasingly massive \<^emph>\<open>digital information\<close> available
incites numerous research efforts summarized under the labels ``semantic web'',
``integrated document management'', or any form of advanced ``semantic'' text processing.
The central role in these technologies, that are increasingly important in jurisprudence,
medical research and life-sciences in order to tame their respective publication tsunamies,
is played by \<^emph>\<open>document ontologies\<close>, \<^ie>, a machine-readable form of meta-data attached to
document-elements as well as their document discourse. In order to make these techniques
applicable to the area of \<^emph>\<open>formal theory development\<close>,
the following is needed:
These technologies are increasingly important in jurisprudence, medical research and
life-sciences in order to tame their respective publication tsunamies. The central role
in these technologies is played by \<^emph>\<open>document ontologies\<close>, \<^ie>, a machine-readable form
of meta-data attached to document-elements as well as their document discourse. In order
to make these techniques applicable to the area of \<^emph>\<open>formal theory development\<close>,
the following is needed: \<^vs>\<open>0.2cm\<close>
\<^item> a general mechanism to define and develop \<^emph>\<open>domain-specific\<close> ontologies,
\<^item> this mechanism should be adapted to entities occurring in formal theories,
\<^item> ... that should be adapted to entities occurring in formal theories,
\<^ie>, provide built-in support for types, terms, theorems, proofs, etc.,
\<^item> ways to annotate meta-data generated by ontologies to the document elements,
as ``deep'' as possible, together with strong validation checks,
@ -81,62 +86,56 @@ the following is needed:
@{cite "books/daglib/0032976"}, pp. 39 ff.\<close>}.
\<close>
text\<open>Recently, \<^dof> @{cite "brucker.ea:isabelledof:2019" and "brucker.ea:isabelle-ontologies:2018"}
\<^footnote>\<open>The official releases are available on \<^url>\<open>https://zenodo.org/record/3370483#.YfWg6S-B1qt\<close>, the
developer version on \<^url>\<open>https://github.com/logicalhacking/Isabelle_DOF\<close>\<close>
text\<open> \<^vs>\<open>-0.2cm\<close>
Recently, \<^dof> @{cite "brucker.ea:isabelledof:2019" and "brucker.ea:isabelle-ontologies:2018"}
\<^footnote>\<open>The official releases are available at \<^url>\<open>https://zenodo.org/record/3370483#.YfWg6S-B1qt\<close>, the
developer version at \<^url>\<open>https://github.com/logicalhacking/Isabelle_DOF\<close>.\<close>
has been designed as an Isabelle component that attempts to answer these needs.
\<^dof> generates from ontology definitions directly integrated into Isabelle theories
typed meta-data, that may be annotated to a number of document elements and that were
validated ``on-the-fly'' during the general continuous type and proof-checking process
in the Prover IDE (Isabelle/PIDE). Thus, \<^dof> profits and extends Isabelle's
document-centric view on code, definitions, proofs, text-elements and other modeling
elements.
in an IDE (Isabelle/PIDE). Thus, we extend the document-centric view on code, definitions,
proofs, text-elements, etc., prevailing in the Isabelle system framework.
In more detail, the schema of \<^dof> text elements --- whose syntax follows closely
the corresponding Isabelle standard elements, except that these do not
posses the brackets with the meta-data --- looks as follows:
@{theory_text [display,indent=10, margin=70]
\<open>
text*[label::classid, attr\<^sub>1=E\<^sub>1, ... attr\<^sub>n=E\<^sub>n]\<open> some formal text \<close>
\<close>}
while code-elements have the form:
In more detail, \<^dof> introduces a number of ``ontology aware'' text-elements with analogous
syntax to standard ones. The difference is a bracket with meta-data of the form: \<^vs>\<open>-0.3cm\<close>
@{theory_text [display,indent=10, margin=70]
\<open>
text*[label::classid, attr\<^sub>1=E\<^sub>1, ... attr\<^sub>n=E\<^sub>n]\<open> some semi-formal text \<close>
ML*[label::classid, attr\<^sub>1=E\<^sub>1, ... attr\<^sub>n=E\<^sub>n]\<open> some SML code \<close>
...
\<close>}
which means for each element that a meta-data object is created and associated to it.
This meta-data can be referenced via its label and used in further computations in text -
or code elements.
\<^vs>\<open>-0.3cm\<close> In these \<^dof> elements, a meta-data object is created and associated to it. This
meta-data can be referenced via its label and used in further computations in text or code.
%; the details will be explained in the subsequent section.
Admittedly, Isabelle is not the first system that comes into one's mind when
writing a scientific paper, a book, or a larger technical documentation.
However, it has a typesetting system inside which is in the
tradition of document generation systems such as mkd, Document! X, Doxygen,
Javadoc, etc., and which embed formal content elements such as formula pretty-prints
into formal text. In Isabelle, these embedded meta-text elements using references
to the context represent a machine-checked macro called \<^emph>\<open>antiquotation\<close>.
Admittedly, Isabelle is not the first system that comes into one's mind when writing a scientific
paper, a book, or a larger technical documentation. However, it has a typesetting system inside
which is in the tradition of document generation systems such as mkd, Document! X, Doxygen,
Javadoc, etc., and which embed formal content such as formula pretty-prints into semi-formal text
or code. The analogous mechanism the Isabelle system provides is a machine-checked macro
called \<^emph>\<open>antiquotation\<close> that depends on the logical context of the document element.
With standard Isabelle antiquotations, for example, the following text element
inside the integrated source will appear in Isabelle/PIDE as follows:
of the integrated source will appear in Isabelle/PIDE as follows: \<^vs>\<open>-0.3cm\<close>
@{theory_text [display,indent=10, margin=70]
\<open>
text\<open> According to the reflexivity axiom @{thm refl}, we obtain in \<Gamma>
for @{term "fac 5"} the result @{value "fac 5"}.\<close>
\<close>}
In the generated document represented in the generated \<^LaTeX> or HTML output, it is shown as:
\<^vs>\<open>-0.5cm\<close> In the corresponding generated \<^LaTeX> or HTML output, this looks like this:
\<^vs>\<open>-0.1cm\<close>
@{theory_text [display,indent=10, margin=70]
\<open>According to the reflexivity axiom \<open>x = x\<close>, we obtain in \<Gamma> for \<open>fac 5\<close> the result \<open>120\<close>.\<close>
}
where the meta-texts \<open>@{thm refl}\<close> ("give the presentation of theorem 'refl'"),
\<^vs>\<open>-0.1cm\<close>where the meta-texts \<open>@{thm refl}\<close> ("give the presentation of theorem 'refl'"),
\<open>@{term "fac 5"}\<close> ("parse and type-check 'fac 5' in the previous logical context")
and \<open>@{value "fac 5"}\<close> ("compile and execute 'fac 5' according to its
definitions") are built-in antiquotations in \<^hol>.
One distinguishing feature of \<^dof> is that specific antiquotations were generated from
an ontology rather than being hard-coded into the Isabelle system infrastructure.
One distinguishing feature of \<^dof> is that specific antiquotations \<^emph>\<open>were generated from
an ontology\<close> rather than being hard-coded into the Isabelle system infrastructure.
\<close>
(*
@ -166,24 +165,31 @@ and typed reference mechanisms inside text- and ML-contexts.
*)
text\<open>
In this paper, we extend prior versions of \<^dof> by
\<^enum> a new form of contexts, namely \<^emph>\<open>term contexts\<close>. Thus, annotations generated
from \<^dof> may also occur in \<open>\<lambda>\<close>-terms used to denote meta-data, and
text\<open>In this paper, we extend prior versions of \<^dof> by
\<^enum> support of antiquotions in a new class of contexts, namely \<^emph>\<open>term contexts\<close>
(rather than SML code or semi-formal text). Thus, annotations generated
from \<^dof> may also occur in \<open>\<lambda>\<close>-terms used to denote meta-data.
\<^enum> formal, machine-checked invariants on meta-data, which correspond to the concept of
"rules" in ontology languages such as OWL, and which can be specified in
"rules" in OWL or "constraints" in UML, and which can be specified in
common HOL \<open>\<lambda>\<close>-term syntax.
\<close>
text\<open>
Beyond the gain of expressivity in \<^dof> ontologies, these features pave the way
for advanced queries of elements inside an integrated document, and for formal proofs
over the relations/translations of ontologies and ontology-instances --- The latter
question raised scientific interest under the label "ontology alignment" for which
we therefore present a (partial) solution. To sum up, we completed \<^dof> to a
text\<open> For example, the \<^dof> evaluation command taking a HOL-expression:
@{theory_text [display,indent=10, margin=70]
\<open> value*[ass::Assertion, relev=2::int] \<open>mapfilter (\<lambda> \<sigma>. relev \<sigma> > 2) @{instance_of \<open>Assertion\<close>}\<close>\<close>
}
where \<^dof> command \<open>value*\<close> type-checks, expands in an own validation phase
the \<open>instance_of\<close>-term antiquotation, and evaluates the resulting HOL expression
above. Assuming an ontology providing the class \<open>Assertion\<close> having at least the
integer attribute \<open>relev\<close>, the command finally creates an instance of \<open>Assertion\<close> and
binds this to the label \<open>ass\<close> for further use.
Beyond the gain of expressivity in \<^dof> ontologies, term-antiquotations pave the way
for advanced queries of elements inside an integrated source, and invariants
allow for formal proofs over the relations/translations of ontologies and ontology-instances.
The latter question raised scientific interest under the label "ontology alignment" for
which we therefore present a formal solution. To sum up, we completed \<^dof> to a
a fairly rich, ITP-oriented ontology language, which is a concrete proposal for the
Isabelle community for a deeper structuring of the Archive of Formal Proofs (AFP;
\<^url>\<open>https://www.isa-afp.org\<close>).
ITP community allowing a deeper structuring of mathematical libraries such as the AFP.
\<close>