Merge branch 'master' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF
This commit is contained in:
commit
a78b1a4bfc
|
@ -37,7 +37,9 @@ text*[abs::abstract,
|
||||||
\<open> \isadof provides an implementation of \dof on top of Isabelle/HOL.
|
\<open> \isadof provides an implementation of \dof on top of Isabelle/HOL.
|
||||||
\dof itself is a novel framework for \<^emph>\<open>defining\<close> ontologies
|
\dof itself is a novel framework for \<^emph>\<open>defining\<close> ontologies
|
||||||
and \<^emph>\<open>enforcing\<close> them during document development and document
|
and \<^emph>\<open>enforcing\<close> them during document development and document
|
||||||
evolution. A major goal of \dof is the integrated development of
|
evolution. \isadof targets use-cases such as mathematical texts referring
|
||||||
|
to a theory development or technical reports requiring a particular structure.
|
||||||
|
A major application of \dof is the integrated development of
|
||||||
formal certification documents (\eg, for Common Criteria or CENELEC
|
formal certification documents (\eg, for Common Criteria or CENELEC
|
||||||
50128) that require consistency across both formal and informal
|
50128) that require consistency across both formal and informal
|
||||||
arguments.
|
arguments.
|
||||||
|
@ -45,10 +47,14 @@ text*[abs::abstract,
|
||||||
\isadof is integrated into Isabelle's IDE, which
|
\isadof is integrated into Isabelle's IDE, which
|
||||||
allows for smooth ontology development as well as immediate
|
allows for smooth ontology development as well as immediate
|
||||||
ontological feedback during the editing of a document.
|
ontological feedback during the editing of a document.
|
||||||
|
Its checking facilities leverage the collaborative
|
||||||
|
development of documents required to be consistent with an
|
||||||
|
underlying ontological structure.
|
||||||
|
|
||||||
In this paper, 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 key
|
concepts of \dof's Ontology Definition Language (ODL) and describe
|
||||||
aspects of the technology of its implementation. \isadof is the
|
comprehensively its major commands. Many examples show typical best-practice
|
||||||
|
applications of the system. \isadof is the
|
||||||
first ontology language supporting machine-checked
|
first ontology language supporting machine-checked
|
||||||
links between the formal and informal parts in an LCF-style
|
links between the formal and informal parts in an LCF-style
|
||||||
interactive theorem proving environment.
|
interactive theorem proving environment.
|
||||||
|
|
|
@ -42,11 +42,11 @@ 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
|
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.
|
the instances of a subclass to be instances of the super-class.
|
||||||
|
|
||||||
To adress this challenge, we present developed the Document Ontology Framework (\dof). \dof is
|
To adress this challenge, we present the Document Ontology Framework (\dof) and an
|
||||||
designed for building scalable and user-friendly tools on top of interactive theorem provers,
|
implementation of DOF called \isadof. \dof is designed for building scalable and user-friendly
|
||||||
and an implementation of DOF called \isadof. \isadof is a novel framework, extending of
|
tools on top of interactive theorem provers. \isadof is a novel framework, implemented as extension of
|
||||||
Isabelle/HOL, to \<^emph>\<open>model\<close> typed ontologies and to \<^emph>\<open>enforce\<close> them during document evolution. Based
|
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
|
on Isabelle's 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
|
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
|
\<^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
|
||||||
|
@ -124,8 +124,8 @@ text\<open>
|
||||||
\<^item> for the implementation of \isadof~@{cite "brucker.ea:isabelledof:2019"}:
|
\<^item> for the implementation of \isadof~@{cite "brucker.ea:isabelledof:2019"}:
|
||||||
\begin{quote}\small
|
\begin{quote}\small
|
||||||
A.~D. Brucker and B.~Wolff. \isadof: Design and implementation. In P.~{\"O}lveczky and
|
A.~D. Brucker and B.~Wolff. \isadof: Design and implementation. In P.~{\"O}lveczky and
|
||||||
G.~Sala{\"u}n, editors, \<^emph>\<open>Software Engineering and Formal Methods (SEFM)\<close>, Lecture Notes
|
G.~Sala{\"u}n, editors, \<^emph>\<open>Software Engineering and Formal Methods (SEFM)\<close>, number 11724 in
|
||||||
in Computer Science. Springer-Verlag, Heidelberg, 2019.
|
Lecture Notes in Computer Science. Springer-Verlag, Heidelberg, 2019.
|
||||||
\end{quote}
|
\end{quote}
|
||||||
A \BibTeX-entry is available at:
|
A \BibTeX-entry is available at:
|
||||||
\url{https://www.brucker.ch/bibliography/abstract/brucker.ea-isabelledof-2019}.
|
\url{https://www.brucker.ch/bibliography/abstract/brucker.ea-isabelledof-2019}.
|
||||||
|
|
|
@ -350,7 +350,7 @@ text\<open>
|
||||||
characters in definitions that need to make use of a entries in an aux-file.
|
characters in definitions that need to make use of a entries in an aux-file.
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
subsubsection\<open>Common Ontology Library (COL)\<close>
|
subsection\<open>Common Ontology Library (COL)\<close>
|
||||||
|
|
||||||
text\<open>\isadof uses the concept of implicit abstract classes (or: \emph{shadow classes}).
|
text\<open>\isadof uses the concept of implicit abstract classes (or: \emph{shadow classes}).
|
||||||
These refer to the set of possible \inlineisar+doc_class+ declarations that posses a number
|
These refer to the set of possible \inlineisar+doc_class+ declarations that posses a number
|
||||||
|
@ -359,7 +359,7 @@ of attributes with their types in common. Shadow classes represent an implicit r
|
||||||
for certain \isadof commands.
|
for certain \isadof commands.
|
||||||
|
|
||||||
shadow classes will find concrete instances in COL, but \isadof text elements do not \emph{depend}
|
shadow classes will find concrete instances in COL, but \isadof text elements do not \emph{depend}
|
||||||
on our COL definitions: Ontology developers are free to use to build own instances for these
|
on our COL definitions: Ontology developers are free to build own class instances for these
|
||||||
shadow classes, with own attributes and, last not least, own definitions of invariants independent
|
shadow classes, with own attributes and, last not least, own definitions of invariants independent
|
||||||
from ours.
|
from ours.
|
||||||
|
|
||||||
|
|
|
@ -1,16 +1,3 @@
|
||||||
(*************************************************************************
|
|
||||||
* Copyright (C)
|
|
||||||
* 2019 The University of Exeter
|
|
||||||
* 2018-2019 The University of Paris-Saclay
|
|
||||||
* 2018 The University of Sheffield
|
|
||||||
*
|
|
||||||
* License:
|
|
||||||
* This program can be redistributed and/or modified under the terms
|
|
||||||
* of the 2-clause BSD-style license.
|
|
||||||
*
|
|
||||||
* SPDX-License-Identifier: BSD-2-Clause
|
|
||||||
*************************************************************************)
|
|
||||||
|
|
||||||
structure RegExpChecker : sig
|
structure RegExpChecker : sig
|
||||||
type 'a equal
|
type 'a equal
|
||||||
type num
|
type num
|
||||||
|
|
Loading…
Reference in New Issue