Initial commit: CICM 2018 paper as example for the scholarly paper ontology.
|
@ -0,0 +1,762 @@
|
|||
(*<*)
|
||||
theory IsaDofApplications
|
||||
imports "../../ontologies/scholarly_paper"
|
||||
begin
|
||||
(*>*)
|
||||
|
||||
title*[tit::title]\<open>Using The Isabelle Ontology Framework\<close>
|
||||
subtitle*[stit::subtitle]\<open>Linking the Formal with the Informal\<close>
|
||||
|
||||
text*[adb::author, email="''a.brucker@sheffield.ac.uk''", orcid="''0000-0002-6355-1200''",
|
||||
affiliation="''University of Sheffield, Sheffield, UK''"] \<open>Achim D. Brucker\<close>
|
||||
text*[idir::author, email="''idir.aitsadoune@centralesupelec.fr''",
|
||||
affiliation = "''CentraleSupelec, Paris, France''"] \<open>Idir Ait-Sadoune\<close>
|
||||
text*[paolo::author,email="''paolo.crisafulli@irt-systemx.fr''",
|
||||
affiliation = "''IRT-SystemX, Paris, France''"] \<open>Paolo Crisafulli\<close>
|
||||
text*[bu::author, email="''wolff@lri.fr''",
|
||||
affiliation="''Universit\\'e Paris-Sud, Paris, France''"] \<open>Burkhart Wolff\<close>
|
||||
|
||||
|
||||
text*[abs::abstract, keywordlist="[''Ontology'',''Ontological Modeling'',''Isabelle/DOF'']"]{*
|
||||
While Isabelle is mostly known as part of Isabelle/HOL (an interactive
|
||||
theorem prover), it actually provides a framework for developing a wide
|
||||
spectrum of applications. A particular strength
|
||||
of the Isabelle framework is the combination of text editing, formal verification,
|
||||
and code generation.
|
||||
|
||||
Up to now, Isabelle's document preparation system lacks a mechanism
|
||||
for ensuring the structure of different document types (as, e.g.,
|
||||
required in certification processes) in general and, in particular,
|
||||
mechanism for linking informal and formal parts of a document.
|
||||
|
||||
In this paper, we present \isadof, a novel Document Ontology Framework
|
||||
on top of Isabelle. \isadof allows for conventional typesetting
|
||||
\emph{as well} as formal development. We show how to model document
|
||||
ontologies inside \isadof, how to use the resulting meta-information
|
||||
for enforcing a certain document structure, and discuss ontology-specific IDE support.
|
||||
*}
|
||||
|
||||
section*[intro::introduction]{* Introduction *}
|
||||
text*[introtext::introduction]{*
|
||||
The linking of the \emph{formal} to the \emph{informal} is perhaps the
|
||||
most pervasive challenge in the digitization of knowledge and its
|
||||
propagation. This challenge incites numerous research efforts
|
||||
summarized under the labels ``semantic web'', ``data mining'', or any
|
||||
form of advanced ``semantic'' text processing. A key role in
|
||||
structuring this linking play \emph{document ontologies} (also called
|
||||
\emph{vocabulary} in the semantic web
|
||||
community~\cite{w3c:ontologies:2015}), \ie, a machine-readable form of
|
||||
the structure of documents as well as the document discourse.
|
||||
Such ontologies can be used for the scientific discourse within scholarly
|
||||
articles, mathematical libraries, and in the engineering discourse
|
||||
of standardized software certification documents\cite{boulanger:cenelec-50128:2015,cc:cc-part3:2006}.
|
||||
Further applications are the domain-specific discourse in juridical texts or medical reports.
|
||||
In general, an ontology is a formal explicit description of \emph{concepts}
|
||||
in a domain of discourse (called \emph{classes}), properties of each concept
|
||||
describing \emph{attributes} of the concept, as well 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.
|
||||
|
||||
The main objective of this paper is to present \isadof, a novel
|
||||
framework 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 changes,
|
||||
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 \emph{may contain}
|
||||
Isabelle/HOL definitions and proofs like mathematical articles, tech-reports and
|
||||
scientific papers---as the present one, which is written in \isadof
|
||||
itself. \isadof is a plugin into the Isabelle/Isar
|
||||
framework in the style of~\cite{wenzel.ea:building:2007}.
|
||||
*}
|
||||
|
||||
(* declaring the forward references used in the subsequent section *)
|
||||
declare_reference*[bgrnd::text_section]
|
||||
declare_reference*[isadof::text_section]
|
||||
declare_reference*[ontomod::text_section]
|
||||
declare_reference*[ontopide::text_section]
|
||||
declare_reference*[conclusion::text_section]
|
||||
|
||||
text{* The plan of the paper is follows: we start by introducing the underlying
|
||||
Isabelel sytem (@{docitem_ref (unchecked) \<open>bgrnd\<close>}) followed by presenting the
|
||||
essentials of \isadof and its ontology language (@{docitem_ref (unchecked) \<open>isadof\<close>}).
|
||||
It follows @{docitem_ref (unchecked) \<open>ontomod\<close>}, where we present three application
|
||||
scenarios from the point of view of the ontology modeling. In @{docitem_ref (unchecked) \<open>ontopide\<close>}
|
||||
we discuss the user-interaction generated from the ontological definitions. Finally, we draw
|
||||
conclusions and discuss related work in @{docitem_ref (unchecked) \<open>conclusion\<close>}. *}
|
||||
|
||||
section*[bgrnd::text_section,
|
||||
text_section.main_author="Some(@{docitem ''adb''}::author)"]
|
||||
{* Background: The Isabelle System *}
|
||||
text{*
|
||||
While Isabelle is widely perceived as an interactive theorem prover
|
||||
for HOL (Higher-order Logic)~\cite{nipkow.ea:isabelle:2002}, we
|
||||
would like to emphasize the view that Isabelle is far more than that:
|
||||
it is the \emph{Eclipse of Formal Methods Tools}. This refers to the
|
||||
``\textsl{generic system framework of Isabelle/Isar underlying recent
|
||||
versions of Isabelle. Among other things, Isar provides an
|
||||
infrastructure for Isabelle plug-ins, comprising extensible state
|
||||
components and extensible syntax that can be bound to ML
|
||||
programs. Thus, the Isabelle/Isar architecture may be understood as
|
||||
an extension and refinement of the traditional `LCF approach', with
|
||||
explicit infrastructure for building derivative
|
||||
\emph{systems}.}''~\cite{wenzel.ea:building:2007}
|
||||
|
||||
The current system framework offers moreover the following features:
|
||||
\begin{compactitem}
|
||||
\item a build management grouping components into to pre-compiled sessions,
|
||||
\item a prover IDE (PIDE) framework~\cite{wenzel:asynchronous:2014} with
|
||||
various front-ends
|
||||
\item documentation - and code generators,
|
||||
\item an extensible front-end language Isabelle/Isar, and,
|
||||
\item last but not least, an LCF style, generic theorem prover kernel as
|
||||
the most prominent and deeply integrated system component.
|
||||
\end{compactitem}
|
||||
*}
|
||||
|
||||
figure*[architecture::figure,relative_width="''100''",
|
||||
src="''figures/isabelle-architecture''"]
|
||||
{* The system architecture of Isabelle (left-hand side) and the
|
||||
asynchronous communication between the Isabelle system and
|
||||
the IDE (right-hand side). *}
|
||||
|
||||
text{* The Isabelle system architecture shown in @{docitem_ref \<open>architecture\<close>}
|
||||
comes with many layers, with Standard ML (SML) at the bottom layer as implementation
|
||||
language. The architecture actually foresees a \emph{Nano-Kernel} (our terminology) which
|
||||
resides in the SML structure \texttt{Context}. This structure provides a kind of container called
|
||||
\emph{context} providing an identity, an ancestor-list as well as typed, user-defined state
|
||||
for components (plugins) such as \isadof. On top of the latter, the LCF-Kernel, tactics,
|
||||
automated proof procedures as well as specific support for higher specification constructs
|
||||
were built. *}
|
||||
|
||||
text{* We would like to detail the documentation generation of the architecture,
|
||||
which is based on literate specification commands such as \inlineisar+section+ \ldots,
|
||||
\inlineisar+subsection+ \ldots, \inlineisar+text+ \ldots, etc.
|
||||
Thus, a user can add a simple text:
|
||||
\begin{isar}
|
||||
text\<Open>This is a description.\<Close>
|
||||
\end{isar}
|
||||
These text-commands can be arbitrarily mixed with other commands stating definitions, proofs, code, etc.,
|
||||
and will result in the corresponding output in generated \LaTeX{} or HTML documents.
|
||||
Now, \emph{inside} the textual content, it is possible to embed a \emph{text-antiquotation}:
|
||||
\begin{isar}
|
||||
text\<Open>According to the reflexivity axiom \at{thm refl}, we obtain in \<Gamma>
|
||||
for \at{term "fac 5"} the result \at{value "fac 5"}.\<Close>
|
||||
\end{isar}
|
||||
which is represented in the generated output by:
|
||||
\begin{out}
|
||||
According to the reflexivity axiom $x = x$, we obtain in $\Gamma$ for $\operatorname{fac} 5$
|
||||
the result $120$.
|
||||
\end{out}
|
||||
where \inlineisar+refl+ is actually the reference to the axiom of reflexivity in HOL.
|
||||
For the antiquotation \inlineisar+\at{value "fac 5"}+ we assume the usual definition for
|
||||
\inlineisar+fac+ in HOL.
|
||||
*}
|
||||
|
||||
text{* Thus, antiquotations can refer to formal content, can be type-checked before being
|
||||
displayed and can be used for calculations before actually being typeset. When editing,
|
||||
Isabelle's PIDE offers auto-completion and error-messages while typing the above
|
||||
\emph{semi-formal} content. *}
|
||||
|
||||
section*[isadof::text_section,
|
||||
text_section.main_author="Some(@{docitem ''adb''}::author)"]
|
||||
{* \isadof *}
|
||||
|
||||
text{* An \isadof document consists of three components:
|
||||
\begin{compactitem}
|
||||
\item the @{emph \<open>ontology definition\<close>} (which is an Isabelle theory file with definitions
|
||||
for document-classes and all auxiliary datatypes.
|
||||
\item the @{emph \<open>core\<close>} of the document itself which is an Isabelle theory
|
||||
importing the ontology definition. \isadof provides an own family of text-element
|
||||
commands such as \inlineisar+title*+, \inlineisar+section*+, \inlineisar+text*+, etc.,
|
||||
which can be annotated with meta-information defined in the underlying ontology definition.
|
||||
\item the @{emph \<open>layout definition\<close>} for the given ontology exploiting this meta-information.
|
||||
\end{compactitem}
|
||||
\isadof is a novel Isabelle system component providing specific support for all these three parts.
|
||||
Note that the document core @{emph \<open>may\<close>}, but @{emph \<open>must\<close>} not
|
||||
use Isabelle definitions or proofs for checking the formal content---the
|
||||
present paper is actually an example of a document not containing any proof.
|
||||
|
||||
The document generation process of \isadof is currently restricted to \LaTeX, which means
|
||||
that the layout is defined by a set of \LaTeX{} style files. Several layout
|
||||
definitions for one ontology are possible and pave the way that different @{emph \<open>views\<close>} for
|
||||
the same central document were generated, addressing the needs of different purposes and/or target
|
||||
readers.
|
||||
|
||||
While the ontology and the layout definition will have to be developed by an expert
|
||||
with knowledge over Isabelle and \isadof and the back end technology depending on the layout
|
||||
definition, the core is intended to require only minimal knowledge of these two. Document core
|
||||
authors @{emph \<open>can\<close>} use \LaTeX{} commands in their source, but this limits the possibility
|
||||
of using different representation technologies, \eg, HTML, and increases the risk of arcane
|
||||
error-messages in generated \LaTeX{}.
|
||||
|
||||
The \isadof ontology specification language consists basically on a notation for
|
||||
document classes, where the attributes were typed with HOL-types and can be instantiated
|
||||
by terms HOL-terms, \ie, the actual parsers and type-checkers of the Isabelle system were reused.
|
||||
This has the particular advantage that \isadof commands can be arbitrarily mixed with
|
||||
Isabelle/HOL commands providing the machinery for type declarations and term specifications such
|
||||
as enumerations. In particular, document class definitions provide:
|
||||
\begin{compactitem}
|
||||
\item a HOL-type for each document class as well as inheritance,
|
||||
\item support for attributes with HOL-types and optional default values,
|
||||
\item support for overriding of attribute defaults but not overloading, and
|
||||
\item text-elements annotated with document classes; they are mutable
|
||||
instances of document classes.
|
||||
\end{compactitem}
|
||||
Attributes referring to other ontological concepts are called \emph{links}.
|
||||
The HOL-types inside the document specification language support built-in types for Isabelle/HOL \inlineisar+typ+'s,
|
||||
\inlineisar+term+'s, and \inlineisar+thm+'s reflecting internal Isabelle's internal types
|
||||
for these entities; when denoted in HOL-terms to instantiate an attribute, for example, there is a
|
||||
specific syntax (called \emph{inner syntax antiquotations}) that is checked by \isadof
|
||||
for consistency.
|
||||
|
||||
Document classes can have a \inlineisar+where+ clause containing a regular
|
||||
expression over class names. Classes with such a \inlineisar+where+ were called \emph{monitor classes}.
|
||||
While document classes and their inheritance relation structure meta-data of text-elements
|
||||
in an object-oriented manner, monitor classes enforce structural organization
|
||||
of documents via the language specified by the regular expression
|
||||
enforcing a sequence of text-elements that must belong to the corresponding classes.
|
||||
|
||||
To start using \isadof, one creates an Isabelle project (with the name
|
||||
\inlinebash{IsaDofApplications}):
|
||||
\begin{bash}
|
||||
isabelle DOF_mkroot -o scholarly_paper -t lncs -d IsaDofApplications
|
||||
\end{bash}
|
||||
where the \inlinebash{-o scholarly_paper} specifies the ontology for writing scientific articles and
|
||||
\inlinebash{-t lncs} specifies the use of Springer's \LaTeX-configuration for the Lecture Notes in Computer Science series. The project
|
||||
can be formally checked, including the generation of the article in PDF using the
|
||||
following command:
|
||||
\begin{bash}
|
||||
isabelle build -d . IsaDofApplications
|
||||
\end{bash}
|
||||
*}
|
||||
|
||||
section*[ontomod::technical]{* Modeling Ontologies in \isadof *}
|
||||
text{* In this section, we will use the \isadof document ontology language
|
||||
for three different application scenarios: for scholarly papers, for mathematical
|
||||
exam sheets as well as standardization documents where the concepts of the
|
||||
standard are captured in the ontology. For space reasons, we will concentrate in all three
|
||||
cases on aspects of the modeling due to space limitations.
|
||||
*}
|
||||
subsection*[scholar_onto::example]{* The Scholar Paper Scenario: Eating One's Own Dog Food. *}
|
||||
text{* The following ontology is a simple ontology modeling scientific papers. In this
|
||||
\isadof application scenario, we deliberately refrain from integrating references to
|
||||
(Isabelle) formal content in order demonstrate that \isadof is not a framework from
|
||||
Isabelle users to Isabelle users only.
|
||||
Of course, such references can be added easily and represent a particular strength
|
||||
of \isadof.
|
||||
|
||||
\begin{figure}
|
||||
\begin{isar}
|
||||
doc_class title =
|
||||
short_title :: "string option" <= None
|
||||
|
||||
doc_class subtitle =
|
||||
abbrev :: "string option" <= None
|
||||
|
||||
doc_class author =
|
||||
affiliation :: "string"
|
||||
|
||||
doc_class abstract =
|
||||
keyword_list :: "string list" <= None
|
||||
|
||||
doc_class text_section =
|
||||
main_author :: "author option" <= None
|
||||
todo_list :: "string list" <= "[]"
|
||||
\end{isar}
|
||||
\caption{The core of the ontology definition for writing scholarly papers.}
|
||||
\label{fig:paper-onto-core}
|
||||
\end{figure}
|
||||
The first part of the ontology \inlineisar+scholarly_paper+ (see \autoref{fig:paper-onto-core})
|
||||
contains the document class definitions
|
||||
with the usual text-elements of a scientific paper. The attributes \inlineisar+short_title+,
|
||||
\inlineisar+abbrev+ etc are introduced with their types as well as their default values.
|
||||
Our model prescribes an optional \inlineisar+main_author+ and a todo-list attached to an arbitrary
|
||||
text section; since instances of this class are mutable (meta)-objects of text-elements, they
|
||||
can be modified arbitrarily through subsequent text and of course globally during text evolution.
|
||||
Since \inlineisar+author+ is a HOL-type internally generated by \isadof framework and can therefore
|
||||
appear in the \inlineisar+main_author+ attribute of the \inlineisar+text_section+ class;
|
||||
semantic links between concepts can be modeled this way.
|
||||
|
||||
The translation of its content to, \eg, Springer's \LaTeX{} setup for the Lecture Notes in Computer
|
||||
Science Series, as required by many scientific conferences, is mostly straight-forward. *}
|
||||
|
||||
figure*[fig1::figure, spawn_columns=False,relative_width="''95''",
|
||||
src="''figures/Dogfood-Intro''"]
|
||||
{* Ouroboros I: This paper from inside \ldots *}
|
||||
|
||||
text{* @{docitem_ref \<open>fig1\<close>} shows the corresponding view in the Isabelle/PIDE of the present paper.
|
||||
Note that the text uses \isadof's own text-commands containing the meta-information provided by
|
||||
the underlying ontology.
|
||||
We proceed by a definition of \inlineisar+introduction+'s, which we define as the extension of
|
||||
\inlineisar+text_section+ which is intended to capture common infrastructure:
|
||||
\begin{isar}
|
||||
doc_class introduction = text_section +
|
||||
comment :: string
|
||||
\end{isar}
|
||||
As a consequence of the definition as extension, the \inlineisar+introduction+ class
|
||||
inherits the attributes \inlineisar+main_author+ and \inlineisar+todo_list+ together with
|
||||
the corresponding default values.
|
||||
|
||||
As a variant of the introduction, we could add here an attribute that contains the formal
|
||||
claims of the article --- either here, or, for example, in the keyword list of the abstract.
|
||||
As type, one could use either the built-in type \inlineisar+term+ (for syntactically correct,
|
||||
but not necessarily proven entity) or \inlineisar+thm+ (for formally proven entities). It suffices
|
||||
to add the line:
|
||||
\begin{isar}
|
||||
claims :: "thm list"
|
||||
\end{isar}
|
||||
and to extent the \LaTeX-style accordingly to handle the additional field.
|
||||
Note that \inlineisar+term+ and \inlineisar+thm+ are types reflecting the core-types of the
|
||||
Isabelle kernel. In a corresponding conclusion section, one could model analogously an
|
||||
achievement section; by programming a specific compliance check in SML, the implementation
|
||||
of automated forms of validation check for specific categories of papers is envisageable.
|
||||
Since this requires deeper knowledge in Isabelle programming, however, we consider this out
|
||||
of the scope of this paper.
|
||||
|
||||
|
||||
We proceed more or less conventionally by the subsequent sections (\autoref{fig:paper-onto-sections})
|
||||
\begin{figure}
|
||||
\begin{isar}
|
||||
doc_class technical = text_section +
|
||||
definition_list :: "string list" <= "[]"
|
||||
|
||||
doc_class example = text_section +
|
||||
comment :: string
|
||||
|
||||
doc_class conclusion = text_section +
|
||||
main_author :: "author option" <= None
|
||||
|
||||
doc_class related_work = conclusion +
|
||||
main_author :: "author option" <= None
|
||||
|
||||
doc_class bibliography =
|
||||
style :: "string option" <= "''LNCS''"
|
||||
\end{isar}
|
||||
\caption{Various types of sections of a scholarly papers.}
|
||||
\label{fig:paper-onto-sections}
|
||||
\end{figure}
|
||||
and finish with a monitor class definition that enforces a textual ordering
|
||||
in the document core by a regular expression (\autoref{fig:paper-onto-monitor}).
|
||||
\begin{figure}
|
||||
\begin{isar}
|
||||
doc_class article =
|
||||
trace :: "(title + subtitle + author+ abstract +
|
||||
introduction + technical + example +
|
||||
conclusion + bibliography) list"
|
||||
where "(title ~~ \<lbrakk>subtitle\<rbrakk> ~~ \<lbrace>author\<rbrace>$^+$+ ~~ abstract ~~
|
||||
introduction ~~ \<lbrace>technical || example\<rbrace>$^+$ ~~ conclusion ~~
|
||||
bibliography)"
|
||||
\end{isar}
|
||||
\caption{A monitor for the scholarly paper ontology.}
|
||||
\label{fig:paper-onto-monitor}
|
||||
\end{figure}
|
||||
*}
|
||||
text{* We might wish to add a component into our ontology that models figures to be included into
|
||||
the document. This boils down to the exercise of modeling structured data in the style of a
|
||||
functional programming language in HOL and to reuse the implicit HOL-type inside a suitable document
|
||||
class \inlineisar+figure+:
|
||||
\begin{isar}
|
||||
datatype placement = h | t | b | ht | hb
|
||||
doc_class figure = text_section +
|
||||
relative_width :: "string" (* percent of textwidth *)
|
||||
src :: "string"
|
||||
placement :: placement
|
||||
spawn_columns :: bool <= True
|
||||
\end{isar}
|
||||
*}
|
||||
(*
|
||||
doc_class side_by_side_figure = figure +
|
||||
anchor :: "string"
|
||||
caption :: "string"
|
||||
relative_width2 :: "string" (* percent of textwidth *)
|
||||
src2 :: "string"
|
||||
anchor2 :: "string"
|
||||
caption2 :: "string"*)
|
||||
text{* Alternatively, by including the HOL-libraries for rationals, it is possible to
|
||||
use fractions or even mathematical reals. This must be counterbalanced by syntactic
|
||||
and semantic convenience. Choosing the mathematical reals, \eg, would have the drawback that
|
||||
attribute evaluation could be substantially more complicated.*}
|
||||
|
||||
figure*[fig_figures::figure, spawn_columns=False,relative_width="''85''",
|
||||
src="''figures/Dogfood-figures''"]
|
||||
{* Ouroboros II: figures \ldots *}
|
||||
|
||||
text{* The document class \inlineisar+figure+ --- supported by the \isadof text command
|
||||
\inlineisar+figure*+ --- makes it possible to express the pictures and diagrams in this paper
|
||||
such as @{docitem_ref \<open>fig_figures\<close>}.
|
||||
*}
|
||||
|
||||
subsection*[mathex_onto::example]{* The Math-Exam Scenario *}
|
||||
text{* The Math-Exam Scenario is an application with mixed formal and
|
||||
semi-formal content. It addresses applications where the author of the exam is not present
|
||||
during the exam and the preparation requires a very rigorous process, as the french
|
||||
\emph{baccaleaureat} and exams at The University of Sheffield.
|
||||
|
||||
We assume that the content has four different types of addressees, which have a different
|
||||
\emph{view} on the integrated document
|
||||
\begin{compactitem}
|
||||
\item the @{emph \<open>setter\<close>}, \ie, the author of the exam,
|
||||
\item the @{emph \<open>checker\<close>}, \ie, an internal person that checks the exam for feasibility
|
||||
and non-ambiguity,
|
||||
\item the @{emph \<open>external examiner\<close>}, \ie, an external person that checks the exam for
|
||||
feasibility and non-ambiguity, and
|
||||
\item the @{emph \<open>student\<close>}, \ie, the addressee of the exam.
|
||||
\end{compactitem}
|
||||
The latter quality assurance mechanism is used in many universities,
|
||||
where for organizational reasons the execution of an exam takes place in facilities
|
||||
where the author of the exam is not expected to be physically present.
|
||||
Furthermore, we assume a simple grade system (thus, some calculation is required).
|
||||
|
||||
\begin{figure}
|
||||
\begin{isar}
|
||||
doc_class Author = ...
|
||||
datatype Subject = algebra | geometry | statistical
|
||||
datatype Grade = A1 | A2 | A3
|
||||
|
||||
doc_class Header = examTitle :: string
|
||||
examSubject :: Subject
|
||||
date :: string
|
||||
timeAllowed :: int -- minutes
|
||||
|
||||
datatype ContentClass = setter
|
||||
| checker
|
||||
| external_examiner
|
||||
| student
|
||||
|
||||
doc_class Exam_item =
|
||||
concerns :: "ContentClass set"
|
||||
|
||||
doc_class Exam_item =
|
||||
concerns :: "ContentClass set"
|
||||
|
||||
type_synonym SubQuestion = string
|
||||
\end{isar}
|
||||
\caption{The core of the ontology modeling math exams.}
|
||||
\label{fig:onto-exam}
|
||||
\end{figure}
|
||||
The heart of this ontology (see \autoref{fig:onto-exam}) is an alternation of questions and answers,
|
||||
where the answers can consist of simple yes-no answers (QCM style check-boxes) or lists of formulas.
|
||||
Since we do not
|
||||
assume familiarity of the students with Isabelle (\inlineisar+term+ would assume that this is a
|
||||
parse-able and type-checkable entity), we basically model a derivation as a sequence of strings
|
||||
(see \autoref{fig:onto-questions}).
|
||||
\begin{figure}
|
||||
\begin{isar}
|
||||
doc_class Answer_Formal_Step = Exam_item +
|
||||
justification :: string
|
||||
"term" :: "string"
|
||||
|
||||
doc_class Answer_YesNo = Exam_item +
|
||||
step_label :: string
|
||||
yes_no :: bool -- \<open>for checkboxes\<close>
|
||||
|
||||
datatype Question_Type =
|
||||
formal | informal | mixed
|
||||
|
||||
doc_class Task = Exam_item +
|
||||
level :: Level
|
||||
type :: Question_Type
|
||||
subitems :: "(SubQuestion *
|
||||
(Answer_Formal_Step list + Answer_YesNo) list) list"
|
||||
concerns :: "ContentClass set" <= "UNIV"
|
||||
mark :: int
|
||||
doc_class Exercise = Exam_item +
|
||||
type :: Question_Type
|
||||
content :: "(Task) list"
|
||||
concerns :: "ContentClass set" <= "UNIV"
|
||||
mark :: int
|
||||
\end{isar}
|
||||
\caption{An exam can contain different types of questions.}
|
||||
\label{fig:onto-questions}
|
||||
\end{figure}
|
||||
|
||||
In many institutions, it makes sense to have a rigorous process of validation
|
||||
for exam subjects: is the initial question correct? Is a proof in the sense of the
|
||||
question possible? We model the possibility that the @{term examiner} validates a
|
||||
question by a sample proof validated by Isabelle (see \autoref{fig:onto-exam-monitor}). In our scenario this sample proofs
|
||||
are completely @{emph \<open>intern\<close>}, \ie, not exposed to the students but just additional
|
||||
material for the internal review process of the exam.
|
||||
\begin{figure}
|
||||
\begin{isar}
|
||||
doc_class Validation =
|
||||
tests :: "term list" <="[]"
|
||||
proofs :: "thm list" <="[]"
|
||||
|
||||
doc_class Solution = Exam_item +
|
||||
content :: "Exercise list"
|
||||
valids :: "Validation list"
|
||||
concerns :: "ContentClass set" <= "{setter,checker,external_examiner}"
|
||||
|
||||
doc_class MathExam=
|
||||
content :: "(Header + Author + Exercise) list"
|
||||
global_grade :: Grade
|
||||
where "\<lbrace>Author\<rbrace>$^+$ ~~ Header ~~ \<lbrace>Exercise ~~ Solution\<rbrace>$^+$ "
|
||||
\end{isar}
|
||||
\caption{Validating exams.}
|
||||
\label{fig:onto-exam-monitor}
|
||||
\end{figure}
|
||||
*}
|
||||
|
||||
|
||||
declare_reference*["fig_qcm"::figure]
|
||||
|
||||
text{* Using the \LaTeX{} package hyperref, it is possible to conceive an interactive
|
||||
exam-sheets with multiple-choice and/or free-response elements
|
||||
(see @{docitem_ref (unchecked) \<open>fig_qcm\<close>}). With the
|
||||
help of the latter, it is possible that students write in a browser a formal mathematical
|
||||
derivation---as part of an algebra exercise, for example---which is submitted to the examiners
|
||||
electronically. *}
|
||||
figure*[fig_qcm::figure, spawn_columns=False,relative_width="''90''",
|
||||
src="''figures/InteractiveMathSheet''"]
|
||||
{* A Generated QCM Fragment \ldots *}
|
||||
|
||||
subsection*[cenelec_onto::example]{* The Certification Scenario following CENELEC *}
|
||||
text{* Documents to be provided in formal certifications (such as CENELEC
|
||||
50126/50128, the DO-178B/C, or Common Criteria) can much profit from the control of ontological consistency:
|
||||
a lot of an evaluators work consists in tracing down the links from requirements over
|
||||
assumptions down to elements of evidence, be it in the models, the code, or the tests.
|
||||
In a certification process, traceability becomes a major concern; and providing
|
||||
mechanisms to ensure complete traceability already at the development of the
|
||||
global document will clearly increase speed and reduce risk and cost of a
|
||||
certification process. Making the link-structure machine-checkable, be it between requirements,
|
||||
assumptions, their implementation and their discharge by evidence (be it tests, proofs, or
|
||||
authoritative arguments), is therefore natural and has the potential to decrease the cost
|
||||
of developments targeting certifications. Continuously checking the links between the formal
|
||||
and the semi-formal parts of such documents is particularly valuable during the (usually
|
||||
collaborative) development effort.
|
||||
|
||||
As in many other cases, formal certification documents come with an own terminology and
|
||||
pragmatics of what has to be demonstrated and where, and how the trace-ability of requirements through
|
||||
design-models over code to system environment assumptions has to be assured.
|
||||
*}
|
||||
text{* In the sequel, we present a simplified version of an ontological model used in a
|
||||
case-study~\cite{bezzecchi.ea:making:2018}. We start with an introduction of the concept of requirement
|
||||
(see \autoref{fig:conceptual}).
|
||||
\begin{figure}
|
||||
\begin{isar}
|
||||
doc_class requirement = long_name :: "string option"
|
||||
|
||||
doc_class requirement_analysis = no :: "nat"
|
||||
where "requirement_item +"
|
||||
|
||||
doc_class hypothesis = requirement +
|
||||
hyp_type :: hyp_type <= physical (* default *)
|
||||
|
||||
datatype ass_kind = informal | semiformal | formal
|
||||
|
||||
doc_class assumption = requirement +
|
||||
assumption_kind :: ass_kind <= informal
|
||||
\end{isar}
|
||||
\caption{Modeling requirements.}
|
||||
\label{fig:conceptual}
|
||||
\end{figure}
|
||||
Such ontologies can be enriched by larger explanations and examples, which may help
|
||||
the team of engineers substantially when developing the central document for a certification,
|
||||
like an explication what is precisely the difference between an \emph{hypothesis} and an
|
||||
\emph{assumption} in the context of the evaluation standard. Since the PIDE makes for each
|
||||
document class its definition available by a simple mouse-click, this kind on meta-knowledge
|
||||
can be made far more accessible during the document evolution.
|
||||
|
||||
For example, the term of category @{emph \<open>assumption\<close>} is used for domain-specific assumptions.
|
||||
It has formal, semi-formal and informal sub-categories. They have to be
|
||||
tracked and discharged by appropriate validation procedures within a
|
||||
certification process, by it by test or proof. It is different from a hypothesis, which is
|
||||
globally assumed and accepted.
|
||||
|
||||
In the sequel, the category @{emph \<open>exported constraint\<close>} (or @{emph \<open>ec\<close>} for short)
|
||||
is used for formal assumptions, that arise during the analysis,
|
||||
design or implementation and have to be tracked till the final
|
||||
evaluation target, and discharged by appropriate validation procedures
|
||||
within the certification process, by it by test or proof. A particular class of interest
|
||||
is the category @{emph \<open>safety related application condition\<close>} (or @{emph \<open>srac\<close>}
|
||||
for short) which is used for @{emph \<open>ec\<close>}'s that establish safety properties
|
||||
of the evaluation target. Their track-ability throughout the certification
|
||||
is therefore particularly critical. This is naturally modeled as follows:
|
||||
\begin{isar}
|
||||
doc_class ec = assumption +
|
||||
assumption_kind :: ass_kind <= (*default *) formal
|
||||
|
||||
doc_class srac = ec +
|
||||
assumption_kind :: ass_kind <= (*default *) formal
|
||||
\end{isar}
|
||||
*}
|
||||
|
||||
section*[ontopide::technical]{* Ontology-based IDE support *}
|
||||
text{* We present a selection of interaction scenarios @{example \<open>scholar_onto\<close>}
|
||||
and @{example \<open>cenelec_onto\<close>} with Isabelle/PIDE instrumented by \isadof.
|
||||
*}
|
||||
subsection*[scholar_pide::example]{* A Scholarly Paper *}
|
||||
text{* In \autoref{fig-Dogfood-II-bgnd1} and \autoref{fig-bgnd-text_section} we show how
|
||||
hovering over links permits to explore its meta-information.
|
||||
Clicking on a document class identifier permits to hyperlink into the corresponding
|
||||
class definition (\autoref{fig:Dogfood-IV-jumpInDocCLass}); hovering over an attribute-definition
|
||||
(which is qualified in order to disambiguate; \autoref{fig:Dogfood-V-attribute}).
|
||||
*}
|
||||
|
||||
side_by_side_figure*["text-elements"::side_by_side_figure,anchor="''fig-Dogfood-II-bgnd1''"
|
||||
,caption="''Exploring a Reference of a Text-Element.''"
|
||||
,relative_width="''48''"
|
||||
,src="''figures/Dogfood-II-bgnd1''"
|
||||
,anchor2="''fig-bgnd-text_section''"
|
||||
,caption2="''Exploring the class of a text element.''"
|
||||
,relative_width2="''47''"
|
||||
,src2="''figures/Dogfood-III-bgnd-text_section''"
|
||||
]{* Exploring text elements. *}
|
||||
|
||||
side_by_side_figure*["hyperlinks"::side_by_side_figure,anchor="''fig:Dogfood-IV-jumpInDocCLass''"
|
||||
,caption="''Hyperlink to Class-Definition.''"
|
||||
,relative_width="''48''"
|
||||
,src="''figures/Dogfood-IV-jumpInDocCLass''"
|
||||
,anchor2="''fig:Dogfood-V-attribute''"
|
||||
,caption2="''Exploring an attribute.''"
|
||||
,relative_width2="''47''"
|
||||
,src2="''figures/Dogfood-III-bgnd-text_section''"
|
||||
]{* Hyperlinks. *}
|
||||
|
||||
declare_reference*["figDogfoodVIlinkappl"::figure]
|
||||
text{* An ontological reference application in
|
||||
\autoref{figDogfoodVIlinkappl}: the
|
||||
ontology-dependant antiquotation \inlineisar|@ {example ...}| refers to the corresponding
|
||||
text-elements. Hovering allows for inspection, clicking for jumping to the definition.
|
||||
If the link does not exist or has a non-compatible type, the text is not validated.
|
||||
*}
|
||||
|
||||
figure*[figDogfoodVIlinkappl::figure,relative_width="''80''",
|
||||
src="''figures/Dogfood-V-attribute''"]
|
||||
{* Exploring an attribute (hyperlinked to the class). *}
|
||||
|
||||
subsection*[cenelec_pide::example]{* CENELEC *}
|
||||
declare_reference*[figfig3::figure]
|
||||
text{* The corresponding view in @{docitem_ref (unchecked)
|
||||
\<open>figfig3\<close>} shows core part of a document,
|
||||
coherent to the @{example \<open>cenelec_onto\<close>}. The first sample shows standard Isabelle antiquotations
|
||||
\cite{wenzel:isabelle-isar:2017} into formal entities of a theory. This way, the informal parts
|
||||
of a document get ``formal content'' and become more robust under change.
|
||||
*}
|
||||
figure*[figfig3::figure,relative_width="''80''",
|
||||
src="''figures/antiquotations-PIDE''"]
|
||||
{* Standard antiquotations referring to theory elements.*}
|
||||
|
||||
declare_reference*[figfig5::figure]
|
||||
text{* The subsequent sample in @{docitem_ref (unchecked) \<open>figfig5\<close>} shows the definition of an
|
||||
\emph{safety-related application condition}, a side-condition of a theorem which
|
||||
has the consequence that a certain calculation must be executed sufficiently fast on an embedded
|
||||
device. This condition can not be established inside the formal theory but has to be
|
||||
checked by system integration tests.*}
|
||||
|
||||
figure*[figfig5::figure,relative_width="''80''",
|
||||
src="''figures/srac-definition''"]
|
||||
{* Defining a SRAC reference \ldots *}
|
||||
figure*[figfig7::figure,relative_width="''80''",
|
||||
src="''figures/srac-as-es-application''"]
|
||||
{* Using a SRAC as EC document reference. *}
|
||||
|
||||
text{* Now we reference in @{docitem_ref (unchecked) \<open>figfig7\<close>} this safety-related condition;
|
||||
however, this happens in a context where general \emph{exported constraints} are listed.
|
||||
\isadof's checks establish that this is legal in the given ontology.
|
||||
|
||||
This example shows that ontological modeling is indeed adequate for large technical,
|
||||
collaboratively developed documentations, where modifications can lead easily to incoherence.
|
||||
The current checks help to systematically avoid this type of incoherence between formal and
|
||||
informal parts. *}
|
||||
(*
|
||||
section*[onto_future::technical]{* Monitor Classes *}
|
||||
text{* Besides sub-typing, there is another relation between
|
||||
document classes: a class can be a \emph{monitor} to other ones,
|
||||
which is expressed by the occurrence of a \inlineisar+where+ clause
|
||||
in the document class definition containing a regular
|
||||
expression (see @{example \<open>scholar_onto\<close>}).
|
||||
While class-extension refers to data-inheritance of attributes,
|
||||
a monitor imposes structural constraints -- the order --
|
||||
in which instances of monitored classes may occur. *}
|
||||
|
||||
text{*
|
||||
The control of monitors is done by the commands:
|
||||
\begin{compactitem}
|
||||
\item \inlineisar+open_monitor* + <doc-class>
|
||||
\item \inlineisar+close_monitor* + <doc-class>
|
||||
\end{compactitem}
|
||||
where the automaton of the monitor class is expected
|
||||
to be in a final state. In the final state, user-defined SML
|
||||
Monitors can be nested, so it is possible to "overlay" one or more monitoring
|
||||
classes and imposing different sets of structural constraints in a
|
||||
Classes which are neither directly nor indirectly (via inheritance) mentioned in the
|
||||
monitor are \emph{independent} from a monitor; instances of independent test elements
|
||||
may occur freely. *}
|
||||
*)
|
||||
|
||||
section*[conclusion::conclusion]{* Conclusion and Related Work*}
|
||||
text{* We have demonstrated the use of \isadof, a novel ontology modeling and enforcement
|
||||
IDE deeply integrated into the Isabelle/Isar Framework. The two most distinguishing features are
|
||||
\begin{compactitem}
|
||||
\item \isadof and its ontology language are a strongly typed language that allows
|
||||
for referring (albeit not reasoning) to entities of Isabelle/HOL, most notably types, terms,
|
||||
and (formally proven) theorems, and
|
||||
\item \isadof is supported by the Isabelle/PIDE framework; thus, the advantages of an IDE for
|
||||
text-exploration (which is the type of this link? To which text element does this link refer?
|
||||
Which are the syntactic alternatives here?) were available during editing
|
||||
instead of a post-hoc validation process.
|
||||
\end{compactitem} *}
|
||||
|
||||
text{* Of course, a conventional batch-process also exists which can be used
|
||||
for the validation of large document bases in a conventional continuous build process.
|
||||
This combination of formal and semi-informal elements, as well as a systematic enforcement
|
||||
of the coherence to a document ontology of the latter, is, as we believe, novel and offers
|
||||
a unique potential for the semantic treatment of scientific texts and technical documentations. *}
|
||||
|
||||
text{*
|
||||
To our knowledge, this is the first ontology-driven framework for
|
||||
editing mathematical and technical documents that focuses particularly
|
||||
on documents mixing formal and informal content---a type of documents
|
||||
that is very common in technical certification processes. We see
|
||||
mainly one area of related works: IDEs and text editors that support
|
||||
editing and checking of documents based on an ontology. There is a
|
||||
large group of ontology editors (\eg, Prot{\'e}g{\'e}~\cite{protege},
|
||||
Fluent Editor~\cite{cognitum}, NeOn~\cite{neon}, or
|
||||
OWLGrEd~\cite{owlgred}). With them, we share the support for defining
|
||||
ontologies as well as auto-completion when editing documents based on
|
||||
an ontology. While our ontology definitions are currently based on a
|
||||
textual definition, widely used ontology editors (\eg,
|
||||
OWLGrEd~\cite{owlgred}) also support graphical notations. This could
|
||||
be added to \isadof in the future. A unique feature of \isadof is the
|
||||
deep integration of formal and informal text parts. The only other
|
||||
work in this area wea are aware of is rOntorium~\cite{rontorium}, a plugin
|
||||
for Prot{\'e}g{\'e} that integrates R~\cite{adler:r:2010} into an
|
||||
ontology environment. Here, the main motivation behind this
|
||||
integration is to allow for statistically analyze ontological
|
||||
documents. Thus, this is complementary to our work.
|
||||
*}
|
||||
|
||||
text{* \isadof in its present form has a number of technical short-comings as well
|
||||
as potentials not yet explored. On the long list of the short-comings is the
|
||||
fact that strings inside HOL-terms do not support, for example, Unicode.
|
||||
For the moment, \isadof is conceived as an
|
||||
add-on for Isabelle/HOL; a much deeper integration of \isadof into Isabelle
|
||||
could increase both performance and uniformity. Finally, different target
|
||||
presentation (such as HTML) would be highly desirable in particular for the
|
||||
math exam scenarios. And last but not least, it would be desirable that PIDE
|
||||
itself is ``ontology-aware'' and can, for example, use meta-information
|
||||
to control read- and write accesses of \emph{parts} of documents.
|
||||
*}
|
||||
|
||||
paragraph{* Availability. *}
|
||||
text{* The implementation of the framework, the discussed ontology definitions,
|
||||
and examples are available at
|
||||
\url{https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF/}.*}
|
||||
paragraph{* Acknowledgement. *}
|
||||
text{* This work was partly supported by the framework of IRT SystemX, Paris-Saclay, France,
|
||||
and therefore granted with public funds within the scope of the
|
||||
Program ``Investissements d’Avenir''.*}
|
||||
|
||||
(*<*)
|
||||
end
|
||||
(*>*)
|
||||
|
|
@ -0,0 +1,25 @@
|
|||
session "IsaDofApplications" = Main + (* "Isabelle_DOF" + *)
|
||||
options [document = pdf, document_output = "output", quick_and_dirty = true]
|
||||
theories [document = false]
|
||||
"../../ontologies/scholarly_paper"
|
||||
theories
|
||||
IsaDofApplications
|
||||
document_files
|
||||
"root.tex"
|
||||
"root.bib"
|
||||
"preamble.tex"
|
||||
"build"
|
||||
"lstisadof.sty"
|
||||
"ontologies.tex"
|
||||
"figures/isabelle-architecture.pdf"
|
||||
"figures/Dogfood-Intro.png"
|
||||
"figures/InteractiveMathSheet.png"
|
||||
"figures/Dogfood-II-bgnd1.png"
|
||||
"figures/Dogfood-III-bgnd-text_section.png"
|
||||
"figures/Dogfood-IV-jumpInDocCLass.png"
|
||||
"figures/Dogfood-III-bgnd-text_section.png"
|
||||
"figures/Dogfood-V-attribute.png"
|
||||
"figures/antiquotations-PIDE.png"
|
||||
"figures/srac-definition.png"
|
||||
"figures/srac-as-es-application.png"
|
||||
"figures/Dogfood-figures.png"
|
|
@ -0,0 +1,928 @@
|
|||
% This file was modified by the DOF LaTeX converter, version 0.0.3
|
||||
%
|
||||
\begin{isabellebody}%
|
||||
\setisabellecontext{IsaDofApplications}%
|
||||
%
|
||||
\isadelimtheory
|
||||
%
|
||||
\endisadelimtheory
|
||||
%
|
||||
\isatagtheory
|
||||
%
|
||||
\endisatagtheory
|
||||
{\isafoldtheory}%
|
||||
%
|
||||
\isadelimtheory
|
||||
\ \isanewline
|
||||
%
|
||||
\endisadelimtheory
|
||||
%
|
||||
\isaDofTitle%
|
||||
%
|
||||
[label={tit}, type={title}]%
|
||||
{Using The Isabelle Ontology Framework}%
|
||||
%
|
||||
\isaDofSubtitle%
|
||||
%
|
||||
[label={stit}, type={subtitle}]%
|
||||
{Linking the Formal with the Informal}%
|
||||
%
|
||||
\isaDofTextAuthor%
|
||||
%
|
||||
[label={adb}, type={author}, email={a.brucker{\isacharat}sheffield.ac.uk}, orcid={0000-0002-6355-1200},
|
||||
affiliation={University of Sheffield, Sheffield, UK}]%
|
||||
{Achim D. Brucker}%
|
||||
%
|
||||
\isaDofTextAuthor%
|
||||
%
|
||||
[label={idir}, type={author}, email={idir.aitsadoune{\isacharat}centralesupelec.fr},
|
||||
affiliation = {CentraleSupelec, Paris, France}]%
|
||||
{Idir Ait-Sadoune}%
|
||||
%
|
||||
\isaDofTextAuthor%
|
||||
%
|
||||
[label={paolo}, type={author},email={paolo.crisafulli{\isacharat}irt-systemx.fr},
|
||||
affiliation = {IRT-SystemX, Paris, France}]%
|
||||
{Paolo Crisafulli}%
|
||||
%
|
||||
\isaDofTextAuthor%
|
||||
%
|
||||
[label={bu}, type={author}, email={wolff{\isacharat}lri.fr},
|
||||
affiliation={Universit\'e Paris-Sud, Paris, France}]%
|
||||
{Burkhart Wolff}%
|
||||
%
|
||||
\isaDofTextAbstract%
|
||||
%
|
||||
[label={abs}, type={abstract}, keywordlist={Ontology,Ontological Modeling,Isabelle/DOF}]%
|
||||
{
|
||||
While Isabelle is mostly known as part of Isabelle/HOL (an interactive
|
||||
theorem prover), it actually provides a framework for developing a wide
|
||||
spectrum of applications. A particular strength
|
||||
of the Isabelle framework is the combination of text editing, formal verification,
|
||||
and code generation.
|
||||
|
||||
Up to now, Isabelle's document preparation system lacks a mechanism
|
||||
for ensuring the structure of different document types (as, e.g.,
|
||||
required in certification processes) in general and, in particular,
|
||||
mechanism for linking informal and formal parts of a document.
|
||||
|
||||
In this paper, we present \isadof, a novel Document Ontology Framework
|
||||
on top of Isabelle. \isadof allows for conventional typesetting
|
||||
\emph{as well} as formal development. We show how to model document
|
||||
ontologies inside \isadof, how to use the resulting meta-information
|
||||
for enforcing a certain document structure, and discuss ontology-specific IDE support.}%
|
||||
%
|
||||
\isaDofSectionIntroduction%
|
||||
%
|
||||
[label={intro}, type={introduction}]%
|
||||
{Introduction}%
|
||||
%
|
||||
\isaDofTextIntroduction%
|
||||
%
|
||||
[label={introtext}, type={introduction}]%
|
||||
{
|
||||
The linking of the \emph{formal} to the \emph{informal} is perhaps the
|
||||
most pervasive challenge in the digitization of knowledge and its
|
||||
propagation. This challenge incites numerous research efforts
|
||||
summarized under the labels {\isacharbackquote}{\isacharbackquote}semantic web'', {\isacharbackquote}{\isacharbackquote}data mining'', or any
|
||||
form of advanced {\isacharbackquote}{\isacharbackquote}semantic'' text processing. A key role in
|
||||
structuring this linking play \emph{document ontologies} (also called
|
||||
\emph{vocabulary} in the semantic web
|
||||
community~\cite{w3c:ontologies:2015}), \ie, a machine-readable form of
|
||||
the structure of documents as well as the document discourse.
|
||||
Such ontologies can be used for the scientific discourse within scholarly
|
||||
articles, mathematical libraries, and in the engineering discourse
|
||||
of standardized software certification documents\cite{boulanger:cenelec-50128:2015,cc:cc-part3:2006}.
|
||||
Further applications are the domain-specific discourse in juridical texts or medical reports.
|
||||
In general, an ontology is a formal explicit description of \emph{concepts}
|
||||
in a domain of discourse (called \emph{classes}), properties of each concept
|
||||
describing \emph{attributes} of the concept, as well 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.
|
||||
|
||||
The main objective of this paper is to present \isadof, a novel
|
||||
framework 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 changes,
|
||||
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 \emph{may contain}
|
||||
Isabelle/HOL definitions and proofs like mathematical articles, tech-reports and
|
||||
scientific papers---as the present one, which is written in \isadof
|
||||
itself. \isadof is a plugin into the Isabelle/Isar
|
||||
framework in the style of~\cite{wenzel.ea:building:2007}.}%
|
||||
%
|
||||
\isaDofDeclareReferenceTextSection%
|
||||
%
|
||||
[label={bgrnd}, type={text_section}]%
|
||||
%
|
||||
%
|
||||
\isaDofDeclareReferenceTextSection%
|
||||
%
|
||||
[label={isadof}, type={text_section}]%
|
||||
%
|
||||
%
|
||||
\isaDofDeclareReferenceTextSection%
|
||||
%
|
||||
[label={ontomod}, type={text_section}]%
|
||||
%
|
||||
%
|
||||
\isaDofDeclareReferenceTextSection%
|
||||
%
|
||||
[label={ontopide}, type={text_section}]%
|
||||
%
|
||||
%
|
||||
\isaDofDeclareReferenceTextSection%
|
||||
%
|
||||
[label={conclusion}, type={text_section}]%
|
||||
%
|
||||
\begin{isamarkuptext}%
|
||||
The plan of the paper is follows: we start by introducing the underlying
|
||||
Isabelel sytem (\autoref{bgrnd}) followed by presenting the
|
||||
essentials of \isadof and its ontology language (\autoref{isadof}).
|
||||
It follows \autoref{ontomod}, where we present three application
|
||||
scenarios from the point of view of the ontology modeling. In \autoref{ontopide}
|
||||
we discuss the user-interaction generated from the ontological definitions. Finally, we draw
|
||||
conclusions and discuss related work in \autoref{conclusion}.%
|
||||
\end{isamarkuptext}\isamarkuptrue%
|
||||
%
|
||||
%
|
||||
\isaDofSectionTextSection%
|
||||
%
|
||||
[label={bgrnd}, type={text_section},
|
||||
text_section.main_author={Some({\isacharat}{docitem adb}::author)}]%
|
||||
{Background: The Isabelle System}%
|
||||
%
|
||||
\begin{isamarkuptext}%
|
||||
While Isabelle is widely perceived as an interactive theorem prover
|
||||
for HOL (Higher-order Logic)~\cite{nipkow.ea:isabelle:2002}, we
|
||||
would like to emphasize the view that Isabelle is far more than that:
|
||||
it is the \emph{Eclipse of Formal Methods Tools}. This refers to the
|
||||
``\textsl{generic system framework of Isabelle/Isar underlying recent
|
||||
versions of Isabelle. Among other things, Isar provides an
|
||||
infrastructure for Isabelle plug-ins, comprising extensible state
|
||||
components and extensible syntax that can be bound to ML
|
||||
programs. Thus, the Isabelle/Isar architecture may be understood as
|
||||
an extension and refinement of the traditional `LCF approach', with
|
||||
explicit infrastructure for building derivative
|
||||
\emph{systems}.}''~\cite{wenzel.ea:building:2007}
|
||||
|
||||
The current system framework offers moreover the following features:
|
||||
\begin{compactitem}
|
||||
\item a build management grouping components into to pre-compiled sessions,
|
||||
\item a prover IDE (PIDE) framework~\cite{wenzel:asynchronous:2014} with
|
||||
various front-ends
|
||||
\item documentation - and code generators,
|
||||
\item an extensible front-end language Isabelle/Isar, and,
|
||||
\item last but not least, an LCF style, generic theorem prover kernel as
|
||||
the most prominent and deeply integrated system component.
|
||||
\end{compactitem}%
|
||||
\end{isamarkuptext}\isamarkuptrue%
|
||||
%
|
||||
\isaDofFigure%
|
||||
%
|
||||
[label={architecture}, type={figure},relative_width={100},
|
||||
src={figures/isabelle-architecture}]%
|
||||
{The system architecture of Isabelle (left-hand side) and the
|
||||
asynchronous communication between the Isabelle system and
|
||||
the IDE (right-hand side).}%
|
||||
%
|
||||
\begin{isamarkuptext}%
|
||||
The Isabelle system architecture shown in \autoref{architecture}
|
||||
comes with many layers, with Standard ML (SML) at the bottom layer as implementation
|
||||
language. The architecture actually foresees a \emph{Nano-Kernel} (our terminology) which
|
||||
resides in the SML structure \texttt{Context}. This structure provides a kind of container called
|
||||
\emph{context} providing an identity, an ancestor-list as well as typed, user-defined state
|
||||
for components (plugins) such as \isadof. On top of the latter, the LCF-Kernel, tactics,
|
||||
automated proof procedures as well as specific support for higher specification constructs
|
||||
were built.%
|
||||
\end{isamarkuptext}\isamarkuptrue%
|
||||
%
|
||||
\begin{isamarkuptext}%
|
||||
We would like to detail the documentation generation of the architecture,
|
||||
which is based on literate specification commands such as \inlineisar+section+ \ldots,
|
||||
\inlineisar+subsection+ \ldots, \inlineisar+text+ \ldots, etc.
|
||||
Thus, a user can add a simple text:
|
||||
\begin{isar}
|
||||
text\<Open>This is a description.\<Close>
|
||||
\end{isar}
|
||||
These text-commands can be arbitrarily mixed with other commands stating definitions, proofs, code, etc.,
|
||||
and will result in the corresponding output in generated \LaTeX{} or HTML documents.
|
||||
Now, \emph{inside} the textual content, it is possible to embed a \emph{text-antiquotation}:
|
||||
\begin{isar}
|
||||
text\<Open>According to the reflexivity axiom @{thm refl}, we obtain in \<Gamma>
|
||||
for @{term "fac 5"} the result @{value "fac 5"}.\<Close>
|
||||
\end{isar}
|
||||
which is represented in the generated output by:
|
||||
\begin{out}
|
||||
According to the reflexivity axiom $x = x$, we obtain in $\Gamma$ for $\operatorname{fac} 5$
|
||||
the result $120$.
|
||||
\end{out}
|
||||
where \inlineisar+refl+ is actually the reference to the axiom of reflexivity in HOL.
|
||||
For the antiquotation \inlineisar+@{value "fac 5"}+ we assume the usual definition for
|
||||
\inlineisar+fac+ in HOL.%
|
||||
\end{isamarkuptext}\isamarkuptrue%
|
||||
%
|
||||
\begin{isamarkuptext}%
|
||||
Thus, antiquotations can refer to formal content, can be type-checked before being
|
||||
displayed and can be used for calculations before actually being typeset. When editing,
|
||||
Isabelle's PIDE offers auto-completion and error-messages while typing the above
|
||||
\emph{semi-formal} content.%
|
||||
\end{isamarkuptext}\isamarkuptrue%
|
||||
%
|
||||
\isaDofSectionTextSection%
|
||||
%
|
||||
[label={isadof}, type={text_section},
|
||||
text_section.main_author={Some({\isacharat}{docitem adb}::author)}]%
|
||||
{\isadof}%
|
||||
%
|
||||
\begin{isamarkuptext}%
|
||||
An \isadof document consists of three components:
|
||||
\begin{compactitem}
|
||||
\item the \emph{ontology definition} (which is an Isabelle theory file with definitions
|
||||
for document-classes and all auxiliary datatypes.
|
||||
\item the \emph{core} of the document itself which is an Isabelle theory
|
||||
importing the ontology definition. \isadof provides an own family of text-element
|
||||
commands such as \inlineisar+title*+, \inlineisar+section*+, \inlineisar+text*+, etc.,
|
||||
which can be annotated with meta-information defined in the underlying ontology definition.
|
||||
\item the \emph{layout definition} for the given ontology exploiting this meta-information.
|
||||
\end{compactitem}
|
||||
\isadof is a novel Isabelle system component providing specific support for all these three parts.
|
||||
Note that the document core \emph{may}, but \emph{must} not
|
||||
use Isabelle definitions or proofs for checking the formal content---the
|
||||
present paper is actually an example of a document not containing any proof.
|
||||
|
||||
The document generation process of \isadof is currently restricted to \LaTeX, which means
|
||||
that the layout is defined by a set of \LaTeX{} style files. Several layout
|
||||
definitions for one ontology are possible and pave the way that different \emph{views} for
|
||||
the same central document were generated, addressing the needs of different purposes and/or target
|
||||
readers.
|
||||
|
||||
While the ontology and the layout definition will have to be developed by an expert
|
||||
with knowledge over Isabelle and \isadof and the back end technology depending on the layout
|
||||
definition, the core is intended to require only minimal knowledge of these two. Document core
|
||||
authors \emph{can} use \LaTeX{} commands in their source, but this limits the possibility
|
||||
of using different representation technologies, \eg, HTML, and increases the risk of arcane
|
||||
error-messages in generated \LaTeX{}.
|
||||
|
||||
The \isadof ontology specification language consists basically on a notation for
|
||||
document classes, where the attributes were typed with HOL-types and can be instantiated
|
||||
by terms HOL-terms, \ie, the actual parsers and type-checkers of the Isabelle system were reused.
|
||||
This has the particular advantage that \isadof commands can be arbitrarily mixed with
|
||||
Isabelle/HOL commands providing the machinery for type declarations and term specifications such
|
||||
as enumerations. In particular, document class definitions provide:
|
||||
\begin{compactitem}
|
||||
\item a HOL-type for each document class as well as inheritance,
|
||||
\item support for attributes with HOL-types and optional default values,
|
||||
\item support for overriding of attribute defaults but not overloading, and
|
||||
\item text-elements annotated with document classes; they are mutable
|
||||
instances of document classes.
|
||||
\end{compactitem}
|
||||
Attributes referring to other ontological concepts are called \emph{links}.
|
||||
The HOL-types inside the document specification language support built-in types for Isabelle/HOL \inlineisar+typ+'s,
|
||||
\inlineisar+term+'s, and \inlineisar+thm+'s reflecting internal Isabelle's internal types
|
||||
for these entities; when denoted in HOL-terms to instantiate an attribute, for example, there is a
|
||||
specific syntax (called \emph{inner syntax antiquotations}) that is checked by \isadof
|
||||
for consistency.
|
||||
|
||||
Document classes can have a \inlineisar+where+ clause containing a regular
|
||||
expression over class names. Classes with such a \inlineisar+where+ were called \emph{monitor classes}.
|
||||
While document classes and their inheritance relation structure meta-data of text-elements
|
||||
in an object-oriented manner, monitor classes enforce structural organization
|
||||
of documents via the language specified by the regular expression
|
||||
enforcing a sequence of text-elements that must belong to the corresponding classes.
|
||||
|
||||
To start using \isadof, one creates an Isabelle project (with the name
|
||||
\inlinebash{IsaDofApplications}):
|
||||
\begin{bash}
|
||||
isabelle DOF_mkroot -o scholarly_paper -t lncs -d IsaDofApplications
|
||||
\end{bash}
|
||||
where the \inlinebash{-o scholarly_paper} specifies the ontology for writing scientific articles and
|
||||
\inlinebash{-t lncs} specifies the use of Springer's \LaTeX-configuration for the Lecture Notes in Computer Science series. The project
|
||||
can be formally checked, including the generation of the article in PDF using the
|
||||
following command:
|
||||
\begin{bash}
|
||||
isabelle build -d . IsaDofApplications
|
||||
\end{bash}%
|
||||
\end{isamarkuptext}\isamarkuptrue%
|
||||
%
|
||||
\isaDofSectionTechnical%
|
||||
%
|
||||
[label={ontomod}, type={technical}]%
|
||||
{Modeling Ontologies in \isadof}%
|
||||
%
|
||||
\begin{isamarkuptext}%
|
||||
In this section, we will use the \isadof document ontology language
|
||||
for three different application scenarios: for scholarly papers, for mathematical
|
||||
exam sheets as well as standardization documents where the concepts of the
|
||||
standard are captured in the ontology. For space reasons, we will concentrate in all three
|
||||
cases on aspects of the modeling due to space limitations.%
|
||||
\end{isamarkuptext}\isamarkuptrue%
|
||||
%
|
||||
\isaDofSubsectionExample%
|
||||
%
|
||||
[label={scholar_onto}, type={example}]%
|
||||
{The Scholar Paper Scenario: Eating One's Own Dog Food.}%
|
||||
%
|
||||
\begin{isamarkuptext}%
|
||||
The following ontology is a simple ontology modeling scientific papers. In this
|
||||
\isadof application scenario, we deliberately refrain from integrating references to
|
||||
(Isabelle) formal content in order demonstrate that \isadof is not a framework from
|
||||
Isabelle users to Isabelle users only.
|
||||
Of course, such references can be added easily and represent a particular strength
|
||||
of \isadof.
|
||||
|
||||
\begin{figure}
|
||||
\begin{isar}
|
||||
doc_class title =
|
||||
short_title :: "string option" <= None
|
||||
|
||||
doc_class subtitle =
|
||||
abbrev :: "string option" <= None
|
||||
|
||||
doc_class author =
|
||||
affiliation :: "string"
|
||||
|
||||
doc_class abstract =
|
||||
keyword_list :: "string list" <= None
|
||||
|
||||
doc_class text_section =
|
||||
main_author :: "author option" <= None
|
||||
todo_list :: "string list" <= "[]"
|
||||
\end{isar}
|
||||
\caption{The core of the ontology definition for writing scholarly papers.}
|
||||
\label{fig:paper-onto-core}
|
||||
\end{figure}
|
||||
The first part of the ontology \inlineisar+scholarly_paper+ (see \autoref{fig:paper-onto-core})
|
||||
contains the document class definitions
|
||||
with the usual text-elements of a scientific paper. The attributes \inlineisar+short_title+,
|
||||
\inlineisar+abbrev+ etc are introduced with their types as well as their default values.
|
||||
Our model prescribes an optional \inlineisar+main_author+ and a todo-list attached to an arbitrary
|
||||
text section; since instances of this class are mutable (meta)-objects of text-elements, they
|
||||
can be modified arbitrarily through subsequent text and of course globally during text evolution.
|
||||
Since \inlineisar+author+ is a HOL-type internally generated by \isadof framework and can therefore
|
||||
appear in the \inlineisar+main_author+ attribute of the \inlineisar+text_section+ class;
|
||||
semantic links between concepts can be modeled this way.
|
||||
|
||||
The translation of its content to, \eg, Springer's \LaTeX{} setup for the Lecture Notes in Computer
|
||||
Science Series, as required by many scientific conferences, is mostly straight-forward.%
|
||||
\end{isamarkuptext}\isamarkuptrue%
|
||||
%
|
||||
\isaDofFigure%
|
||||
%
|
||||
[label={fig1}, type={figure}, spawn_columns=False,relative_width={95},
|
||||
src={figures/Dogfood-Intro}]%
|
||||
{Ouroboros I: This paper from inside \ldots}%
|
||||
%
|
||||
\begin{isamarkuptext}%
|
||||
\autoref{fig1} shows the corresponding view in the Isabelle/PIDE of the present paper.
|
||||
Note that the text uses \isadof's own text-commands containing the meta-information provided by
|
||||
the underlying ontology.
|
||||
We proceed by a definition of \inlineisar+introduction+'s, which we define as the extension of
|
||||
\inlineisar+text_section+ which is intended to capture common infrastructure:
|
||||
\begin{isar}
|
||||
doc_class introduction = text_section +
|
||||
comment :: string
|
||||
\end{isar}
|
||||
As a consequence of the definition as extension, the \inlineisar+introduction+ class
|
||||
inherits the attributes \inlineisar+main_author+ and \inlineisar+todo_list+ together with
|
||||
the corresponding default values.
|
||||
|
||||
As a variant of the introduction, we could add here an attribute that contains the formal
|
||||
claims of the article --- either here, or, for example, in the keyword list of the abstract.
|
||||
As type, one could use either the built-in type \inlineisar+term+ (for syntactically correct,
|
||||
but not necessarily proven entity) or \inlineisar+thm+ (for formally proven entities). It suffices
|
||||
to add the line:
|
||||
\begin{isar}
|
||||
claims :: "thm list"
|
||||
\end{isar}
|
||||
and to extent the \LaTeX-style accordingly to handle the additional field.
|
||||
Note that \inlineisar+term+ and \inlineisar+thm+ are types reflecting the core-types of the
|
||||
Isabelle kernel. In a corresponding conclusion section, one could model analogously an
|
||||
achievement section; by programming a specific compliance check in SML, the implementation
|
||||
of automated forms of validation check for specific categories of papers is envisageable.
|
||||
Since this requires deeper knowledge in Isabelle programming, however, we consider this out
|
||||
of the scope of this paper.
|
||||
|
||||
|
||||
We proceed more or less conventionally by the subsequent sections (\autoref{fig:paper-onto-sections})
|
||||
\begin{figure}
|
||||
\begin{isar}
|
||||
doc_class technical = text_section +
|
||||
definition_list :: "string list" <= "[]"
|
||||
|
||||
doc_class example = text_section +
|
||||
comment :: string
|
||||
|
||||
doc_class conclusion = text_section +
|
||||
main_author :: "author option" <= None
|
||||
|
||||
doc_class related_work = conclusion +
|
||||
main_author :: "author option" <= None
|
||||
|
||||
doc_class bibliography =
|
||||
style :: "string option" <= "''LNCS''"
|
||||
\end{isar}
|
||||
\caption{Various types of sections of a scholarly papers.}
|
||||
\label{fig:paper-onto-sections}
|
||||
\end{figure}
|
||||
and finish with a monitor class definition that enforces a textual ordering
|
||||
in the document core by a regular expression (\autoref{fig:paper-onto-monitor}).
|
||||
\begin{figure}
|
||||
\begin{isar}
|
||||
doc_class article =
|
||||
trace :: "(title + subtitle + author+ abstract +
|
||||
introduction + technical + example +
|
||||
conclusion + bibliography) list"
|
||||
where "(title ~~ \<lbrakk>subtitle\<rbrakk> ~~ \<lbrace>author\<rbrace>$^+$+ ~~ abstract ~~
|
||||
introduction ~~ \<lbrace>technical || example\<rbrace>$^+$ ~~ conclusion ~~
|
||||
bibliography)"
|
||||
\end{isar}
|
||||
\caption{A monitor for the scholarly paper ontology.}
|
||||
\label{fig:paper-onto-monitor}
|
||||
\end{figure}%
|
||||
\end{isamarkuptext}\isamarkuptrue%
|
||||
%
|
||||
\begin{isamarkuptext}%
|
||||
We might wish to add a component into our ontology that models figures to be included into
|
||||
the document. This boils down to the exercise of modeling structured data in the style of a
|
||||
functional programming language in HOL and to reuse the implicit HOL-type inside a suitable document
|
||||
class \inlineisar+figure+:
|
||||
\begin{isar}
|
||||
datatype placement = h | t | b | ht | hb
|
||||
doc_class figure = text_section +
|
||||
relative_width :: "string" (* percent of textwidth *)
|
||||
src :: "string"
|
||||
placement :: placement
|
||||
spawn_columns :: bool <= True
|
||||
\end{isar}%
|
||||
\end{isamarkuptext}\isamarkuptrue%
|
||||
%
|
||||
\begin{isamarkuptext}%
|
||||
Alternatively, by including the HOL-libraries for rationals, it is possible to
|
||||
use fractions or even mathematical reals. This must be counterbalanced by syntactic
|
||||
and semantic convenience. Choosing the mathematical reals, \eg, would have the drawback that
|
||||
attribute evaluation could be substantially more complicated.%
|
||||
\end{isamarkuptext}\isamarkuptrue%
|
||||
%
|
||||
\isaDofFigure%
|
||||
%
|
||||
[label={fig_figures}, type={figure}, spawn_columns=False,relative_width={85},
|
||||
src={figures/Dogfood-figures}]%
|
||||
{Ouroboros II: figures \ldots}%
|
||||
%
|
||||
\begin{isamarkuptext}%
|
||||
The document class \inlineisar+figure+ --- supported by the \isadof text command
|
||||
\inlineisar+figure*+ --- makes it possible to express the pictures and diagrams in this paper
|
||||
such as \autoref{fig_figures}.%
|
||||
\end{isamarkuptext}\isamarkuptrue%
|
||||
%
|
||||
\isaDofSubsectionExample%
|
||||
%
|
||||
[label={mathex_onto}, type={example}]%
|
||||
{The Math-Exam Scenario}%
|
||||
%
|
||||
\begin{isamarkuptext}%
|
||||
The Math-Exam Scenario is an application with mixed formal and
|
||||
semi-formal content. It addresses applications where the author of the exam is not present
|
||||
during the exam and the preparation requires a very rigorous process, as the french
|
||||
\emph{baccaleaureat} and exams at The University of Sheffield.
|
||||
|
||||
We assume that the content has four different types of addressees, which have a different
|
||||
\emph{view} on the integrated document
|
||||
\begin{compactitem}
|
||||
\item the \emph{setter}, \ie, the author of the exam,
|
||||
\item the \emph{checker}, \ie, an internal person that checks the exam for feasibility
|
||||
and non-ambiguity,
|
||||
\item the \emph{external examiner}, \ie, an external person that checks the exam for
|
||||
feasibility and non-ambiguity, and
|
||||
\item the \emph{student}, \ie, the addressee of the exam.
|
||||
\end{compactitem}
|
||||
The latter quality assurance mechanism is used in many universities,
|
||||
where for organizational reasons the execution of an exam takes place in facilities
|
||||
where the author of the exam is not expected to be physically present.
|
||||
Furthermore, we assume a simple grade system (thus, some calculation is required).
|
||||
|
||||
\begin{figure}
|
||||
\begin{isar}
|
||||
doc_class Author = ...
|
||||
datatype Subject = algebra | geometry | statistical
|
||||
datatype Grade = A1 | A2 | A3
|
||||
|
||||
doc_class Header = examTitle :: string
|
||||
examSubject :: Subject
|
||||
date :: string
|
||||
timeAllowed :: int -- minutes
|
||||
|
||||
datatype ContentClass = setter
|
||||
| checker
|
||||
| external_examiner
|
||||
| student
|
||||
|
||||
doc_class Exam_item =
|
||||
concerns :: "ContentClass set"
|
||||
|
||||
doc_class Exam_item =
|
||||
concerns :: "ContentClass set"
|
||||
|
||||
type_synonym SubQuestion = string
|
||||
\end{isar}
|
||||
\caption{The core of the ontology modeling math exams.}
|
||||
\label{fig:onto-exam}
|
||||
\end{figure}
|
||||
The heart of this ontology (see \autoref{fig:onto-exam}) is an alternation of questions and answers,
|
||||
where the answers can consist of simple yes-no answers (QCM style check-boxes) or lists of formulas.
|
||||
Since we do not
|
||||
assume familiarity of the students with Isabelle (\inlineisar+term+ would assume that this is a
|
||||
parse-able and type-checkable entity), we basically model a derivation as a sequence of strings
|
||||
(see \autoref{fig:onto-questions}).
|
||||
\begin{figure}
|
||||
\begin{isar}
|
||||
doc_class Answer_Formal_Step = Exam_item +
|
||||
justification :: string
|
||||
"term" :: "string"
|
||||
|
||||
doc_class Answer_YesNo = Exam_item +
|
||||
step_label :: string
|
||||
yes_no :: bool -- \isa{for\ checkboxes}
|
||||
|
||||
datatype Question_Type =
|
||||
formal | informal | mixed
|
||||
|
||||
doc_class Task = Exam_item +
|
||||
level :: Level
|
||||
type :: Question_Type
|
||||
subitems :: "(SubQuestion *
|
||||
(Answer_Formal_Step list + Answer_YesNo) list) list"
|
||||
concerns :: "ContentClass set" <= "UNIV"
|
||||
mark :: int
|
||||
doc_class Exercise = Exam_item +
|
||||
type :: Question_Type
|
||||
content :: "(Task) list"
|
||||
concerns :: "ContentClass set" <= "UNIV"
|
||||
mark :: int
|
||||
\end{isar}
|
||||
\caption{An exam can contain different types of questions.}
|
||||
\label{fig:onto-questions}
|
||||
\end{figure}
|
||||
|
||||
In many institutions, it makes sense to have a rigorous process of validation
|
||||
for exam subjects: is the initial question correct? Is a proof in the sense of the
|
||||
question possible? We model the possibility that the \isa{examiner} validates a
|
||||
question by a sample proof validated by Isabelle (see \autoref{fig:onto-exam-monitor}). In our scenario this sample proofs
|
||||
are completely \emph{intern}, \ie, not exposed to the students but just additional
|
||||
material for the internal review process of the exam.
|
||||
\begin{figure}
|
||||
\begin{isar}
|
||||
doc_class Validation =
|
||||
tests :: "term list" <="[]"
|
||||
proofs :: "thm list" <="[]"
|
||||
|
||||
doc_class Solution = Exam_item +
|
||||
content :: "Exercise list"
|
||||
valids :: "Validation list"
|
||||
concerns :: "ContentClass set" <= "{setter,checker,external_examiner}"
|
||||
|
||||
doc_class MathExam=
|
||||
content :: "(Header + Author + Exercise) list"
|
||||
global_grade :: Grade
|
||||
where "\<lbrace>Author\<rbrace>$^+$ ~~ Header ~~ \<lbrace>Exercise ~~ Solution\<rbrace>$^+$ "
|
||||
\end{isar}
|
||||
\caption{Validating exams.}
|
||||
\label{fig:onto-exam-monitor}
|
||||
\end{figure}%
|
||||
\end{isamarkuptext}\isamarkuptrue%
|
||||
%
|
||||
\isaDofDeclareReferenceFigure%
|
||||
%
|
||||
[label={{fig_qcm}}, type={figure}]%
|
||||
%
|
||||
\begin{isamarkuptext}%
|
||||
Using the \LaTeX{} package hyperref, it is possible to conceive an interactive
|
||||
exam-sheets with multiple-choice and/or free-response elements
|
||||
(see \autoref{fig_qcm}). With the
|
||||
help of the latter, it is possible that students write in a browser a formal mathematical
|
||||
derivation---as part of an algebra exercise, for example---which is submitted to the examiners
|
||||
electronically.%
|
||||
\end{isamarkuptext}\isamarkuptrue%
|
||||
%
|
||||
%
|
||||
\isaDofFigure%
|
||||
%
|
||||
[label={fig_qcm}, type={figure}, spawn_columns=False,relative_width={90},
|
||||
src={figures/InteractiveMathSheet}]%
|
||||
{A Generated QCM Fragment \ldots}%
|
||||
%
|
||||
\isaDofSubsectionExample%
|
||||
%
|
||||
[label={cenelec_onto}, type={example}]%
|
||||
{The Certification Scenario following CENELEC}%
|
||||
%
|
||||
\begin{isamarkuptext}%
|
||||
Documents to be provided in formal certifications (such as CENELEC
|
||||
50126/50128, the DO-178B/C, or Common Criteria) can much profit from the control of ontological consistency:
|
||||
a lot of an evaluators work consists in tracing down the links from requirements over
|
||||
assumptions down to elements of evidence, be it in the models, the code, or the tests.
|
||||
In a certification process, traceability becomes a major concern; and providing
|
||||
mechanisms to ensure complete traceability already at the development of the
|
||||
global document will clearly increase speed and reduce risk and cost of a
|
||||
certification process. Making the link-structure machine-checkable, be it between requirements,
|
||||
assumptions, their implementation and their discharge by evidence (be it tests, proofs, or
|
||||
authoritative arguments), is therefore natural and has the potential to decrease the cost
|
||||
of developments targeting certifications. Continuously checking the links between the formal
|
||||
and the semi-formal parts of such documents is particularly valuable during the (usually
|
||||
collaborative) development effort.
|
||||
|
||||
As in many other cases, formal certification documents come with an own terminology and
|
||||
pragmatics of what has to be demonstrated and where, and how the trace-ability of requirements through
|
||||
design-models over code to system environment assumptions has to be assured.%
|
||||
\end{isamarkuptext}\isamarkuptrue%
|
||||
%
|
||||
\begin{isamarkuptext}%
|
||||
In the sequel, we present a simplified version of an ontological model used in a
|
||||
case-study~\cite{bezzecchi.ea:making:2018}. We start with an introduction of the concept of requirement
|
||||
(see \autoref{fig:conceptual}).
|
||||
\begin{figure}
|
||||
\begin{isar}
|
||||
doc_class requirement = long_name :: "string option"
|
||||
|
||||
doc_class requirement_analysis = no :: "nat"
|
||||
where "requirement_item +"
|
||||
|
||||
doc_class hypothesis = requirement +
|
||||
hyp_type :: hyp_type <= physical (* default *)
|
||||
|
||||
datatype ass_kind = informal | semiformal | formal
|
||||
|
||||
doc_class assumption = requirement +
|
||||
assumption_kind :: ass_kind <= informal
|
||||
\end{isar}
|
||||
\caption{Modeling requirements.}
|
||||
\label{fig:conceptual}
|
||||
\end{figure}
|
||||
Such ontologies can be enriched by larger explanations and examples, which may help
|
||||
the team of engineers substantially when developing the central document for a certification,
|
||||
like an explication what is precisely the difference between an \emph{hypothesis} and an
|
||||
\emph{assumption} in the context of the evaluation standard. Since the PIDE makes for each
|
||||
document class its definition available by a simple mouse-click, this kind on meta-knowledge
|
||||
can be made far more accessible during the document evolution.
|
||||
|
||||
For example, the term of category \emph{assumption} is used for domain-specific assumptions.
|
||||
It has formal, semi-formal and informal sub-categories. They have to be
|
||||
tracked and discharged by appropriate validation procedures within a
|
||||
certification process, by it by test or proof. It is different from a hypothesis, which is
|
||||
globally assumed and accepted.
|
||||
|
||||
In the sequel, the category \emph{exported constraint} (or \emph{ec} for short)
|
||||
is used for formal assumptions, that arise during the analysis,
|
||||
design or implementation and have to be tracked till the final
|
||||
evaluation target, and discharged by appropriate validation procedures
|
||||
within the certification process, by it by test or proof. A particular class of interest
|
||||
is the category \emph{safety related application condition} (or \emph{srac}
|
||||
for short) which is used for \emph{ec}'s that establish safety properties
|
||||
of the evaluation target. Their track-ability throughout the certification
|
||||
is therefore particularly critical. This is naturally modeled as follows:
|
||||
\begin{isar}
|
||||
doc_class ec = assumption +
|
||||
assumption_kind :: ass_kind <= (*default *) formal
|
||||
|
||||
doc_class srac = ec +
|
||||
assumption_kind :: ass_kind <= (*default *) formal
|
||||
\end{isar}%
|
||||
\end{isamarkuptext}\isamarkuptrue%
|
||||
%
|
||||
\isaDofSectionTechnical%
|
||||
%
|
||||
[label={ontopide}, type={technical}]%
|
||||
{Ontology-based IDE support}%
|
||||
%
|
||||
\begin{isamarkuptext}%
|
||||
We present a selection of interaction scenarios \autoref{scholar_onto}
|
||||
and \autoref{cenelec_onto} with Isabelle/PIDE instrumented by \isadof.%
|
||||
\end{isamarkuptext}\isamarkuptrue%
|
||||
%
|
||||
\isaDofSubsectionExample%
|
||||
%
|
||||
[label={scholar_pide}, type={example}]%
|
||||
{A Scholarly Paper}%
|
||||
%
|
||||
\begin{isamarkuptext}%
|
||||
In \autoref{fig-Dogfood-II-bgnd1} and \autoref{fig-bgnd-text_section} we show how
|
||||
hovering over links permits to explore its meta-information.
|
||||
Clicking on a document class identifier permits to hyperlink into the corresponding
|
||||
class definition (\autoref{fig:Dogfood-IV-jumpInDocCLass}); hovering over an attribute-definition
|
||||
(which is qualified in order to disambiguate; \autoref{fig:Dogfood-V-attribute}).%
|
||||
\end{isamarkuptext}\isamarkuptrue%
|
||||
%
|
||||
\isaDofSideBySideFigure%
|
||||
%
|
||||
[label={{text-elements}}, type={side_by_side_figure},anchor={fig-Dogfood-II-bgnd1}
|
||||
,caption={Exploring a Reference of a Text-Element.}
|
||||
,relative_width={48}
|
||||
,src={figures/Dogfood-II-bgnd1}
|
||||
,anchor2={fig-bgnd-text_section}
|
||||
,caption2={Exploring the class of a text element.}
|
||||
,relative_width2={47}
|
||||
,src2={figures/Dogfood-III-bgnd-text_section}
|
||||
]%
|
||||
{Exploring text elements.}%
|
||||
%
|
||||
\isaDofSideBySideFigure%
|
||||
%
|
||||
[label={{hyperlinks}}, type={side_by_side_figure},anchor={fig:Dogfood-IV-jumpInDocCLass}
|
||||
,caption={Hyperlink to Class-Definition.}
|
||||
,relative_width={48}
|
||||
,src={figures/Dogfood-IV-jumpInDocCLass}
|
||||
,anchor2={fig:Dogfood-V-attribute}
|
||||
,caption2={Exploring an attribute.}
|
||||
,relative_width2={47}
|
||||
,src2={figures/Dogfood-III-bgnd-text_section}
|
||||
]%
|
||||
{Hyperlinks.}%
|
||||
%
|
||||
\isaDofDeclareReferenceFigure%
|
||||
%
|
||||
[label={{figDogfoodVIlinkappl}}, type={figure}]%
|
||||
%
|
||||
\begin{isamarkuptext}%
|
||||
An ontological reference application in
|
||||
\autoref{figDogfoodVIlinkappl}: the
|
||||
ontology-dependant antiquotation \inlineisar|@ {example ...}| refers to the corresponding
|
||||
text-elements. Hovering allows for inspection, clicking for jumping to the definition.
|
||||
If the link does not exist or has a non-compatible type, the text is not validated.%
|
||||
\end{isamarkuptext}\isamarkuptrue%
|
||||
%
|
||||
%
|
||||
\isaDofFigure%
|
||||
%
|
||||
[label={figDogfoodVIlinkappl}, type={figure},relative_width={80},
|
||||
src={figures/Dogfood-V-attribute}]%
|
||||
{Exploring an attribute (hyperlinked to the class).}%
|
||||
%
|
||||
\isaDofSubsectionExample%
|
||||
%
|
||||
[label={cenelec_pide}, type={example}]%
|
||||
{CENELEC}%
|
||||
%
|
||||
\isaDofDeclareReferenceFigure%
|
||||
%
|
||||
[label={figfig3}, type={figure}]%
|
||||
%
|
||||
\begin{isamarkuptext}%
|
||||
The corresponding view in \autoref{figfig3} shows core part of a document,
|
||||
coherent to the \autoref{cenelec_onto}. The first sample shows standard Isabelle antiquotations
|
||||
\cite{wenzel:isabelle-isar:2017} into formal entities of a theory. This way, the informal parts
|
||||
of a document get ``formal content'' and become more robust under change.%
|
||||
\end{isamarkuptext}\isamarkuptrue%
|
||||
%
|
||||
%
|
||||
\isaDofFigure%
|
||||
%
|
||||
[label={figfig3}, type={figure},relative_width={80},
|
||||
src={figures/antiquotations-PIDE}]%
|
||||
{Standard antiquotations referring to theory elements.}%
|
||||
%
|
||||
\isaDofDeclareReferenceFigure%
|
||||
%
|
||||
[label={figfig5}, type={figure}]%
|
||||
%
|
||||
\begin{isamarkuptext}%
|
||||
The subsequent sample in \autoref{figfig5} shows the definition of an
|
||||
\emph{safety-related application condition}, a side-condition of a theorem which
|
||||
has the consequence that a certain calculation must be executed sufficiently fast on an embedded
|
||||
device. This condition can not be established inside the formal theory but has to be
|
||||
checked by system integration tests.%
|
||||
\end{isamarkuptext}\isamarkuptrue%
|
||||
%
|
||||
%
|
||||
\isaDofFigure%
|
||||
%
|
||||
[label={figfig5}, type={figure},relative_width={80},
|
||||
src={figures/srac-definition}]%
|
||||
{Defining a SRAC reference \ldots}%
|
||||
%
|
||||
\isaDofFigure%
|
||||
%
|
||||
[label={figfig7}, type={figure},relative_width={80},
|
||||
src={figures/srac-as-es-application}]%
|
||||
{Using a SRAC as EC document reference.}%
|
||||
%
|
||||
\begin{isamarkuptext}%
|
||||
Now we reference in \autoref{figfig7} this safety-related condition;
|
||||
however, this happens in a context where general \emph{exported constraints} are listed.
|
||||
\isadof's checks establish that this is legal in the given ontology.
|
||||
|
||||
This example shows that ontological modeling is indeed adequate for large technical,
|
||||
collaboratively developed documentations, where modifications can lead easily to incoherence.
|
||||
The current checks help to systematically avoid this type of incoherence between formal and
|
||||
informal parts.%
|
||||
\end{isamarkuptext}\isamarkuptrue%
|
||||
%
|
||||
\isaDofSectionConclusion%
|
||||
%
|
||||
[label={conclusion}, type={conclusion}]%
|
||||
{Conclusion and Related Work}%
|
||||
%
|
||||
\begin{isamarkuptext}%
|
||||
We have demonstrated the use of \isadof, a novel ontology modeling and enforcement
|
||||
IDE deeply integrated into the Isabelle/Isar Framework. The two most distinguishing features are
|
||||
\begin{compactitem}
|
||||
\item \isadof and its ontology language are a strongly typed language that allows
|
||||
for referring (albeit not reasoning) to entities of Isabelle/HOL, most notably types, terms,
|
||||
and (formally proven) theorems, and
|
||||
\item \isadof is supported by the Isabelle/PIDE framework; thus, the advantages of an IDE for
|
||||
text-exploration (which is the type of this link? To which text element does this link refer?
|
||||
Which are the syntactic alternatives here?) were available during editing
|
||||
instead of a post-hoc validation process.
|
||||
\end{compactitem}%
|
||||
\end{isamarkuptext}\isamarkuptrue%
|
||||
%
|
||||
\begin{isamarkuptext}%
|
||||
Of course, a conventional batch-process also exists which can be used
|
||||
for the validation of large document bases in a conventional continuous build process.
|
||||
This combination of formal and semi-informal elements, as well as a systematic enforcement
|
||||
of the coherence to a document ontology of the latter, is, as we believe, novel and offers
|
||||
a unique potential for the semantic treatment of scientific texts and technical documentations.%
|
||||
\end{isamarkuptext}\isamarkuptrue%
|
||||
%
|
||||
\begin{isamarkuptext}%
|
||||
To our knowledge, this is the first ontology-driven framework for
|
||||
editing mathematical and technical documents that focuses particularly
|
||||
on documents mixing formal and informal content---a type of documents
|
||||
that is very common in technical certification processes. We see
|
||||
mainly one area of related works: IDEs and text editors that support
|
||||
editing and checking of documents based on an ontology. There is a
|
||||
large group of ontology editors (\eg, Prot{\'e}g{\'e}~\cite{protege},
|
||||
Fluent Editor~\cite{cognitum}, NeOn~\cite{neon}, or
|
||||
OWLGrEd~\cite{owlgred}). With them, we share the support for defining
|
||||
ontologies as well as auto-completion when editing documents based on
|
||||
an ontology. While our ontology definitions are currently based on a
|
||||
textual definition, widely used ontology editors (\eg,
|
||||
OWLGrEd~\cite{owlgred}) also support graphical notations. This could
|
||||
be added to \isadof in the future. A unique feature of \isadof is the
|
||||
deep integration of formal and informal text parts. The only other
|
||||
work in this area wea are aware of is rOntorium~\cite{rontorium}, a plugin
|
||||
for Prot{\'e}g{\'e} that integrates R~\cite{adler:r:2010} into an
|
||||
ontology environment. Here, the main motivation behind this
|
||||
integration is to allow for statistically analyze ontological
|
||||
documents. Thus, this is complementary to our work.%
|
||||
\end{isamarkuptext}\isamarkuptrue%
|
||||
%
|
||||
\begin{isamarkuptext}%
|
||||
\isadof in its present form has a number of technical short-comings as well
|
||||
as potentials not yet explored. On the long list of the short-comings is the
|
||||
fact that strings inside HOL-terms do not support, for example, Unicode.
|
||||
For the moment, \isadof is conceived as an
|
||||
add-on for Isabelle/HOL; a much deeper integration of \isadof into Isabelle
|
||||
could increase both performance and uniformity. Finally, different target
|
||||
presentation (such as HTML) would be highly desirable in particular for the
|
||||
math exam scenarios. And last but not least, it would be desirable that PIDE
|
||||
itself is ``ontology-aware'' and can, for example, use meta-information
|
||||
to control read- and write accesses of \emph{parts} of documents.%
|
||||
\end{isamarkuptext}\isamarkuptrue%
|
||||
%
|
||||
\isamarkupparagraph{Availability.%
|
||||
}
|
||||
\isamarkuptrue%
|
||||
%
|
||||
\begin{isamarkuptext}%
|
||||
The implementation of the framework, the discussed ontology definitions,
|
||||
and examples are available at
|
||||
\url{https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF/}.%
|
||||
\end{isamarkuptext}\isamarkuptrue%
|
||||
%
|
||||
\isamarkupparagraph{Acknowledgement.%
|
||||
}
|
||||
\isamarkuptrue%
|
||||
%
|
||||
\begin{isamarkuptext}%
|
||||
This work was partly supported by the framework of IRT SystemX, Paris-Saclay, France,
|
||||
and therefore granted with public funds within the scope of the
|
||||
Program ``Investissements d’Avenir''.%
|
||||
\end{isamarkuptext}\isamarkuptrue%
|
||||
%
|
||||
\isadelimtheory
|
||||
%
|
||||
\endisadelimtheory
|
||||
%
|
||||
\isatagtheory
|
||||
%
|
||||
\endisatagtheory
|
||||
{\isafoldtheory}%
|
||||
%
|
||||
\isadelimtheory
|
||||
%
|
||||
\endisadelimtheory
|
||||
%
|
||||
\end{isabellebody}%
|
||||
%%% Local Variables:
|
||||
%%% mode: latex
|
||||
%%% TeX-master: "root"
|
||||
%%% End:
|
|
@ -0,0 +1,80 @@
|
|||
#!/usr/bin/env bash
|
||||
# Copyright (c) 2018 The University of Sheffield. All rights reserved.
|
||||
# 2018 The University of Paris-Sud. All rights reserved.
|
||||
#
|
||||
# Redistribution and use in source and binary forms, with or without
|
||||
# modification, are permitted provided that the following conditions
|
||||
# are met:
|
||||
# 1. Redistributions of source code must retain the above copyright
|
||||
# notice, this list of conditions and the following disclaimer.
|
||||
# 2. Redistributions in binary form must reproduce the above copyright
|
||||
# notice, this list of conditions and the following disclaimer in
|
||||
# the documentation and/or other materials provided with the
|
||||
# distribution.
|
||||
# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
|
||||
# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
|
||||
# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
|
||||
# FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
|
||||
# COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
|
||||
# INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
|
||||
# BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
|
||||
# LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
|
||||
# CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
|
||||
# LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
|
||||
# ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
|
||||
# POSSIBILITY OF SUCH DAMAGE.
|
||||
#
|
||||
# SPDX-License-Identifier: BSD-2-Clause
|
||||
|
||||
OUTFORMAT=${1:-pdf}
|
||||
NAME=${2:-root}
|
||||
|
||||
set -e
|
||||
|
||||
ROOT_NAME="root_$NAME"
|
||||
[ ! -f "$DIR/$ROOT_NAME.tex" ] && ROOT_NAME="root"
|
||||
|
||||
if [ ! -f $ISABELLE_HOME_USER/DOF/lib/dof_latex_converter.jar ]; then
|
||||
echo ""
|
||||
echo "Warning: Isabelle DOF not installed"
|
||||
echo "========"
|
||||
echo "This is a Isabelle_DOF project. The document preparation requires"
|
||||
echo "the Isabelle_DOF framework. Please obtain the framework by cloning"
|
||||
echo "the Isabelle_DOF git repository, i.e.: "
|
||||
echo " git clone https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF"
|
||||
echo "You can install the framework as follows:"
|
||||
echo " cd Isabelle_DOF/document-generator"
|
||||
echo " ./install"
|
||||
echo ""
|
||||
exit 1
|
||||
fi
|
||||
|
||||
VERSION=$($ISABELLE_TOOL scala $ISABELLE_HOME_USER/DOF/lib/dof_latex_converter.jar -v) || true
|
||||
|
||||
if [ "$VERSION" != "DOF LaTeX converter version 0.0.3" ]; then
|
||||
echo ""
|
||||
echo "Warning: Isabelle DOF version mismatch"
|
||||
echo "========"
|
||||
echo " Build script version: DOF LaTeX converter version 0.0.2"
|
||||
echo " DOF LaTeX Converter version: $VERSION"
|
||||
echo " Please take one of the following actions:"
|
||||
echo " * If the build script is more recent than the converter, "
|
||||
echo " then update the build script from your your Isabelle DOF"
|
||||
echo " installation:"
|
||||
echo " $ISABELLE_HOME_USER/DOF/document-template/build"
|
||||
echo " * If the converter is more recent than the build script,"
|
||||
echo " please update your Isabelle DOF installation."
|
||||
exit 1
|
||||
fi
|
||||
|
||||
$ISABELLE_TOOL scala $ISABELLE_HOME_USER/DOF/lib/dof_latex_converter.jar .
|
||||
|
||||
cp $ISABELLE_HOME_USER/DOF/latex/*.sty .
|
||||
|
||||
$ISABELLE_TOOL latex -o sty "$ROOT_NAME.tex" && \
|
||||
$ISABELLE_TOOL latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \
|
||||
{ [ ! -f "$ROOT_NAME.bib" ] || $ISABELLE_TOOL latex -o bbl "$ROOT_NAME.tex"; } && \
|
||||
{ [ ! -f "$ROOT_NAME.idx" ] || $ISABELLE_TOOL latex -o idx "$ROOT_NAME.tex"; } && \
|
||||
$ISABELLE_TOOL latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \
|
||||
$ISABELLE_TOOL latex -o "$OUTFORMAT" "$ROOT_NAME.tex"
|
||||
|
After Width: | Height: | Size: 14 KiB |
After Width: | Height: | Size: 18 KiB |
After Width: | Height: | Size: 23 KiB |
After Width: | Height: | Size: 85 KiB |
After Width: | Height: | Size: 16 KiB |
After Width: | Height: | Size: 18 KiB |
After Width: | Height: | Size: 75 KiB |
After Width: | Height: | Size: 96 KiB |
After Width: | Height: | Size: 57 KiB |
After Width: | Height: | Size: 67 KiB |
After Width: | Height: | Size: 50 KiB |
|
@ -0,0 +1,149 @@
|
|||
|
||||
\definecolor{OliveGreen} {cmyk}{0.64,0,0.95,0.40}
|
||||
\definecolor{BrickRed} {cmyk}{0,0.89,0.94,0.28}
|
||||
\definecolor{Blue} {cmyk}{1,1,0,0}
|
||||
\definecolor{CornflowerBlue}{cmyk}{0.65,0.13,0,0}
|
||||
|
||||
%%%\lst@BeginAspect[keywords]{isar}
|
||||
\gdef\lst@tagtypes{s}
|
||||
\gdef\lst@TagKey#1#2{%
|
||||
\lst@Delim\lst@tagstyle #2\relax
|
||||
{Tag}\lst@tagtypes #1%
|
||||
{\lst@BeginTag\lst@EndTag}%
|
||||
\@@end\@empty{}}
|
||||
\lst@Key{tag}\relax{\lst@TagKey\@empty{#1}}
|
||||
\lst@Key{tagstyle}{}{\def\lst@tagstyle{#1}}
|
||||
\lst@AddToHook{EmptyStyle}{\let\lst@tagstyle\@empty}
|
||||
\gdef\lst@BeginTag{%
|
||||
\lst@DelimOpen
|
||||
\lst@ifextags\else
|
||||
{\let\lst@ifkeywords\iftrue
|
||||
\lst@ifmarkfirstintag \lst@firstintagtrue \fi}}
|
||||
\lst@AddToHookExe{ExcludeDelims}{\let\lst@ifextags\iffalse}
|
||||
\gdef\lst@EndTag{\lst@DelimClose\lst@ifextags\else}
|
||||
\lst@Key{usekeywordsintag}t[t]{\lstKV@SetIf{#1}\lst@ifusekeysintag}
|
||||
\lst@Key{markfirstintag}f[t]{\lstKV@SetIf{#1}\lst@ifmarkfirstintag}
|
||||
\gdef\lst@firstintagtrue{\global\let\lst@iffirstintag\iftrue}
|
||||
\global\let\lst@iffirstintag\iffalse
|
||||
\lst@AddToHook{PostOutput}{\lst@tagresetfirst}
|
||||
\lst@AddToHook{Output}
|
||||
{\gdef\lst@tagresetfirst{\global\let\lst@iffirstintag\iffalse}}
|
||||
\lst@AddToHook{OutputOther}{\gdef\lst@tagresetfirst{}}
|
||||
\lst@AddToHook{Output}
|
||||
{\ifnum\lst@mode=\lst@tagmode
|
||||
\lst@iffirstintag \let\lst@thestyle\lst@gkeywords@sty \fi
|
||||
\lst@ifusekeysintag\else \let\lst@thestyle\lst@gkeywords@sty\fi
|
||||
\fi}
|
||||
\lst@NewMode\lst@tagmode
|
||||
\gdef\lst@Tag@s#1#2\@empty#3#4#5{%
|
||||
\lst@CArg #1\relax\lst@DefDelimB {}{}%
|
||||
{\ifnum\lst@mode=\lst@tagmode \expandafter\@gobblethree \fi}%
|
||||
#3\lst@tagmode{#5}%
|
||||
\lst@CArg #2\relax\lst@DefDelimE {}{}{}#4\lst@tagmode}%
|
||||
\gdef\lst@BeginCDATA#1\@empty{%
|
||||
\lst@TrackNewLines \lst@PrintToken
|
||||
\lst@EnterMode\lst@GPmode{}\let\lst@ifmode\iffalse
|
||||
\lst@mode\lst@tagmode #1\lst@mode\lst@GPmode\relax\lst@modetrue}
|
||||
%%\lst@EndAspect
|
||||
|
||||
|
||||
|
||||
% \gdef\lst@BeginTag{%
|
||||
% \lst@DelimOpen
|
||||
% \lst@ifextags\else
|
||||
% {\let\lst@ifkeywords\iftrue
|
||||
% \lst@ifmarkfirstintag\lst@firstintagtrue\fi\color{green}}}
|
||||
% \gdef\lst@EndTag{\lst@DelimClose\lst@ifextags\else\color{green}}
|
||||
|
||||
\def\beginlstdelim#1#2#3%
|
||||
{%
|
||||
\def\endlstdelim{\texttt{\textbf{\color{black!60}#2}}\egroup}%
|
||||
\ttfamily\textbf{\color{black!60}#1}\bgroup\rmfamily\color{#3}\aftergroup\endlstdelim%
|
||||
}
|
||||
\newcommand{\subscr}[1]{\ensuremath{_{\mbox{#1}}}}
|
||||
\newcommand{\supscr}[1]{\ensuremath{^{\mbox{#1}}}}
|
||||
\lstdefinestyle{ISAR}{%
|
||||
language=%
|
||||
,basicstyle=\ttfamily%
|
||||
,showspaces=false%
|
||||
,showlines=false%
|
||||
,columns=flexible%
|
||||
,morecomment=[s]{(*}{*)}%
|
||||
% ,moredelim=*[s][\rmfamily]{\{*}{*\}}%
|
||||
,moredelim = **[is][\beginlstdelim{\{*}{*\}}{black}]{\{*}{*\}}
|
||||
,showstringspaces=false%
|
||||
,moredelim=*[is][\supscr]{\\<^bsup>}{\\<^esup>}%
|
||||
,literate={%
|
||||
{...}{\,\ldots\,}3%
|
||||
{\\<Open>}{\ensuremath{\isacartoucheopen}}1%
|
||||
{\\<Close>}{\ensuremath{\isacartoucheclose}}1%
|
||||
{\\<Gamma>}{\ensuremath{\Gamma}}1%
|
||||
{\\<times>}{\ensuremath{\times}}1%
|
||||
{\\<rbrakk>}{\ensuremath{\mathclose{\rbrack\mkern-3mu\rbrack}}}1%
|
||||
{\\<rbrace>}{\ensuremath{\mathclose{\mid\mkern-4.5mu\rbrace}}}1%
|
||||
{\\<lbrakk>}{\ensuremath{\mathopen{\lbrack\mkern-3mu\lbrack}}}1%
|
||||
{\\<lbrace>}{\ensuremath{\mathopen{\lbrace\mkern-4.5mu\mid}}}1%
|
||||
{\\<Rightarrow>}{\ensuremath{\Rightarrow}}1%
|
||||
{\{*}{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}1%
|
||||
{*\}}{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}1%
|
||||
}%
|
||||
% % Defining "tags" (text-antiquotations) based on 1-keywords
|
||||
,tag=**[s]{@\{}{\}}%
|
||||
,tagstyle=\color{CornflowerBlue}%
|
||||
,markfirstintag=true%
|
||||
,keywordstyle=\bfseries%
|
||||
,keywords={}
|
||||
% Defining 2-keywords
|
||||
,keywordstyle=[2]{\color{Blue!60}\bfseries}%
|
||||
,alsoletter={*,-}
|
||||
,morekeywords=[2]{theory, begin, end, ML,section,subsection,paragraph,chapter,text}%
|
||||
%,moredelim=[s][\textit]{<}{>}
|
||||
% Defining 3-keywords
|
||||
,keywordstyle=[3]{\color{OliveGreen!60}\bfseries}%
|
||||
,morekeywords=[3]{doc_class,declare_reference,update_instance*,
|
||||
open_monitor*, close_monitor*, figure*, title*, subtitle*,declare_reference*,section*,text*}%
|
||||
% Defining 4-keywords
|
||||
,keywordstyle=[4]{\color{black!60}\bfseries}%
|
||||
,morekeywords=[4]{where, imports}%
|
||||
% Defining 5-keywords
|
||||
,keywordstyle=[5]{\color{BrickRed!70}\bfseries}%
|
||||
,morekeywords=[5]{datatype, typedecl, consts, theorem}%
|
||||
% Defining 6-keywords
|
||||
,keywordstyle=[6]{\itshape}%
|
||||
,morekeywords=[6]{meta-args, ref, expr, class_id}%
|
||||
%
|
||||
}%
|
||||
%%
|
||||
\lstnewenvironment{isar}[1][]{\lstset{style=ISAR,
|
||||
backgroundcolor=\color{black!2},
|
||||
frame=lines,
|
||||
mathescape=true,
|
||||
basicstyle=\footnotesize\ttfamily,#1}}{}
|
||||
%%%
|
||||
\def\inlineisar{\lstinline[style=ISAR,breaklines=true,mathescape,breakatwhitespace=true]}
|
||||
|
||||
\lstnewenvironment{out}[1][]{\lstset{
|
||||
backgroundcolor=\color{green!2},
|
||||
frame=lines,mathescape,breakatwhitespace=true
|
||||
,columns=flexible%
|
||||
,basicstyle=\footnotesize\rmfamily,#1}}{}
|
||||
|
||||
|
||||
%%%%%%%%%%%%%%%%%%
|
||||
%%%%%%%%%%%%%%%%%%
|
||||
\lstloadlanguages{ML}
|
||||
\lstdefinestyle{sml}{basicstyle=\ttfamily,%
|
||||
commentstyle=\itshape,%
|
||||
keywordstyle=\bfseries\color{CornflowerBlue},%
|
||||
ndkeywordstyle=\color{red},%
|
||||
language=ML,
|
||||
,keywordstyle=[6]{\itshape}%
|
||||
,morekeywords=[6]{args_type}%
|
||||
}%
|
||||
|
||||
\lstnewenvironment{sml}[1][]{\lstset{style=sml,
|
||||
backgroundcolor=\color{Blue!4},
|
||||
frame=lines,
|
||||
basicstyle=\footnotesize\ttfamily,#1}}{}
|
||||
%%%
|
||||
\def\inlinesml{\lstinline[style=sml,breaklines=true,mathescape,breakatwhitespace=true]}
|
|
@ -0,0 +1,17 @@
|
|||
% This file was modified by the DOF LaTeX converter, version 0.0.3
|
||||
%% Copyright (C) 2018 The University of Sheffield
|
||||
%% 2018 The University of Paris-Sud
|
||||
%%
|
||||
%% License:
|
||||
%% This program can be redistributed and/or modified under the terms
|
||||
%% of the LaTeX Project Public License Distributed from CTAN
|
||||
%% archives in directory macros/latex/base/lppl.txt; either
|
||||
%% version 1 of the License, or any later version.
|
||||
%% OR
|
||||
%% The 2-clause BSD-style license.
|
||||
%%
|
||||
%% SPDX-License-Identifier: LPPL-1.0+ OR BSD-2-Clause
|
||||
|
||||
%% This file is used for including the LaTeX ontology mappings.
|
||||
\usepackage{DOF-core}
|
||||
\usepackage{DOF-scholarly_paper}
|
|
@ -0,0 +1,43 @@
|
|||
% This file was modified by the DOF LaTeX converter, version 0.0.3
|
||||
\usepackage[scaled=0.88]{beramono}
|
||||
\usepackage{upquote}
|
||||
\usepackage{textcomp}
|
||||
\usepackage{xcolor}
|
||||
\usepackage{paralist}
|
||||
\usepackage{listings}
|
||||
\usepackage{lstisadof}
|
||||
\usepackage{xspace}
|
||||
\usepackage[draft]{fixme}
|
||||
|
||||
\lstloadlanguages{bash}
|
||||
\lstdefinestyle{bash}{language=bash,
|
||||
,basicstyle=\ttfamily%
|
||||
,showspaces=false%
|
||||
,showlines=false%
|
||||
,columns=flexible%
|
||||
% ,keywordstyle=\bfseries%
|
||||
% Defining 2-keywords
|
||||
,keywordstyle=[1]{\color{BrickRed!60}\bfseries}%
|
||||
% Defining 3-keywords
|
||||
,keywordstyle=[2]{\color{OliveGreen!60}\bfseries}%
|
||||
% Defining 4-keywords
|
||||
,keywordstyle=[3]{\color{black!60}\bfseries}%
|
||||
% Defining 5-keywords
|
||||
,keywordstyle=[4]{\color{Blue!70}\bfseries}%
|
||||
% Defining 6-keywords
|
||||
,keywordstyle=[5]{\itshape}%
|
||||
%
|
||||
}
|
||||
\lstdefinestyle{displaybash}{style=bash,
|
||||
basicstyle=\ttfamily\footnotesize,
|
||||
backgroundcolor=\color{black!2}, frame=lines}%
|
||||
|
||||
\lstnewenvironment{bash}[1][]{\lstset{style=displaybash, #1}}{}
|
||||
\def\inlinebash{\lstinline[style=bash, breaklines=true,columns=fullflexible]}
|
||||
|
||||
\newcommand{\isadof}{Isabelle/DOF\xspace}
|
||||
|
||||
%%% Local Variables:
|
||||
%%% mode: latex
|
||||
%%% TeX-master: "root.tex"
|
||||
%%% End:
|
|
@ -0,0 +1,281 @@
|
|||
@STRING{pub-springer={Springer} }
|
||||
@STRING{pub-springer:adr=""}
|
||||
@STRING{s-lncs = "LNCS" }
|
||||
|
||||
|
||||
@Manual{ wenzel:isabelle-isar:2017,
|
||||
title = {The Isabelle/Isar Reference Manual},
|
||||
author = {Makarius Wenzel},
|
||||
OPTorganization = {},
|
||||
OPTaddress = {},
|
||||
OPTedition = {},
|
||||
OPTmonth = {},
|
||||
year = {2017},
|
||||
note = {Part of the Isabelle distribution.},
|
||||
OPTannote = {}
|
||||
}
|
||||
|
||||
@Book{ adler:r:2010,
|
||||
abstract = {Presents a guide to the R computer language, covering such
|
||||
topics as the user interface, packages, syntax, objects,
|
||||
functions, object-oriented programming, data sets, lattice
|
||||
graphics, regression models, and bioconductor.},
|
||||
added-at = {2013-01-10T22:39:38.000+0100},
|
||||
address = {Sebastopol, CA},
|
||||
author = {Adler, Joseph},
|
||||
isbn = {9780596801700 059680170X},
|
||||
keywords = {R},
|
||||
publisher = {O'Reilly},
|
||||
refid = 432987461,
|
||||
title = {R in a nutshell},
|
||||
year = 2010
|
||||
}
|
||||
|
||||
|
||||
|
||||
@InCollection{ wenzel.ea:building:2007,
|
||||
abstract = {We present the generic system framework of
|
||||
Isabelle/Isarunderlying recent versions of Isabelle. Among
|
||||
other things, Isar provides an infrastructure for Isabelle
|
||||
plug-ins, comprising extensible state components and
|
||||
extensible syntax that can be bound to tactical ML
|
||||
programs. Thus the Isabelle/Isar architecture may be
|
||||
understood as an extension and refinement of the
|
||||
traditional LCF approach, with explicit infrastructure for
|
||||
building derivative systems. To demonstrate the technical
|
||||
potential of the framework, we apply it to a concrete
|
||||
formalmethods tool: the HOL-Z 3.0 environment, which is
|
||||
geared towards the analysis of Z specifications and formal
|
||||
proof of forward-refinements.},
|
||||
author = {Makarius Wenzel and Burkhart Wolff},
|
||||
booktitle = {TPHOLs 2007},
|
||||
editor = {Klaus Schneider and Jens Brandt},
|
||||
language = {USenglish},
|
||||
acknowledgement={none},
|
||||
pages = {352--367},
|
||||
publisher = pub-springer,
|
||||
address = pub-springer:adr,
|
||||
number = 4732,
|
||||
series = s-lncs,
|
||||
title = {Building Formal Method Tools in the {Isabelle}/{Isar}
|
||||
Framework},
|
||||
doi = {10.1007/978-3-540-74591-4_26},
|
||||
year = 2007
|
||||
}
|
||||
|
||||
@Misc{w3c:ontologies:2015,
|
||||
title={Ontologies},
|
||||
organisation={W3c},
|
||||
url={https://www.w3.org/standards/semanticweb/ontology},
|
||||
year=2018
|
||||
}
|
||||
|
||||
@BOOK{boulanger:cenelec-50128:2015,
|
||||
AUTHOR = "Boulanger, Jean-Louis",
|
||||
TITLE = "{CENELEC} 50128 and {IEC} 62279 Standards",
|
||||
PUBLISHER = "Wiley-ISTE",
|
||||
YEAR = "2015",
|
||||
ADDRESS = "Boston",
|
||||
NOTE = "The reference on the standard."
|
||||
}
|
||||
|
||||
@Booklet{ cc:cc-part3:2006,
|
||||
bibkey = {cc:cc-part3:2006},
|
||||
key = {Common Criteria},
|
||||
institution = {Common Criteria},
|
||||
language = {USenglish},
|
||||
month = sep,
|
||||
year = 2006,
|
||||
public = {yes},
|
||||
title = {Common Criteria for Information Technology Security
|
||||
Evaluation (Version 3.1), {Part} 3: Security assurance
|
||||
components},
|
||||
note = {Available as document
|
||||
\href{http://www.commoncriteriaportal.org/public/files/CCPART3V3.1R1.pdf}
|
||||
{CCMB-2006-09-003}},
|
||||
number = {CCMB-2006-09-003},
|
||||
acknowledgement={brucker, 2007-04-24}
|
||||
}
|
||||
|
||||
|
||||
@Book{ nipkow.ea:isabelle:2002,
|
||||
author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
|
||||
title = {Isabelle/HOL---A Proof Assistant for Higher-Order
|
||||
Logic},
|
||||
publisher = pub-springer,
|
||||
address = pub-springer:adr,
|
||||
series = s-lncs,
|
||||
volume = 2283,
|
||||
doi = {10.1007/3-540-45949-9},
|
||||
abstract = {This book is a self-contained introduction to interactive
|
||||
proof in higher-order logic (\acs{hol}), using the proof
|
||||
assistant Isabelle2002. It is a tutorial for potential
|
||||
users rather than a monograph for researchers. The book has
|
||||
three parts.
|
||||
|
||||
1. Elementary Techniques shows how to model functional
|
||||
programs in higher-order logic. Early examples involve
|
||||
lists and the natural numbers. Most proofs are two steps
|
||||
long, consisting of induction on a chosen variable followed
|
||||
by the auto tactic. But even this elementary part covers
|
||||
such advanced topics as nested and mutual recursion. 2.
|
||||
Logic and Sets presents a collection of lower-level tactics
|
||||
that you can use to apply rules selectively. It also
|
||||
describes Isabelle/\acs{hol}'s treatment of sets, functions
|
||||
and relations and explains how to define sets inductively.
|
||||
One of the examples concerns the theory of model checking,
|
||||
and another is drawn from a classic textbook on formal
|
||||
languages. 3. Advanced Material describes a variety of
|
||||
other topics. Among these are the real numbers, records and
|
||||
overloading. Advanced techniques are described involving
|
||||
induction and recursion. A whole chapter is devoted to an
|
||||
extended example: the verification of a security protocol. },
|
||||
year = 2002,
|
||||
acknowledgement={brucker, 2007-02-19},
|
||||
bibkey = {nipkow.ea:isabelle:2002},
|
||||
tags = {noTAG},
|
||||
clearance = {unclassified},
|
||||
timestap = {2008-05-26}
|
||||
}
|
||||
|
||||
|
||||
|
||||
@InProceedings{ wenzel:asynchronous:2014,
|
||||
author = {Makarius Wenzel},
|
||||
title = {Asynchronous User Interaction and Tool Integration in
|
||||
Isabelle/{PIDE}},
|
||||
booktitle = {Interactive Theorem Proving (ITP)},
|
||||
pages = {515--530},
|
||||
year = 2014,
|
||||
crossref = {klein.ea:interactive:2014},
|
||||
doi = {10.1007/978-3-319-08970-6_33},
|
||||
timestamp = {Sun, 21 May 2017 00:18:59 +0200},
|
||||
abstract = { Historically, the LCF tradition of interactive theorem
|
||||
proving was tied to the read-eval-print loop, with
|
||||
sequential and synchronous evaluation of prover commands
|
||||
given on the command-line. This user-interface technology
|
||||
was adequate when R. Milner introduced his LCF proof
|
||||
assistant in the 1970-ies, but it severely limits the
|
||||
potential of current multicore hardware and advanced IDE
|
||||
front-ends.
|
||||
|
||||
Isabelle/PIDE breaks this loop and retrofits the
|
||||
read-eval-print phases into an asynchronous model of
|
||||
document-oriented proof processing. Instead of feeding a
|
||||
sequence of individual commands into the prover process,
|
||||
the primary interface works via edits over a family of
|
||||
document versions. Execution is implicit and managed by the
|
||||
prover on its own account in a timeless and stateless
|
||||
manner. Various aspects of interactive proof checking are
|
||||
scheduled according to requirements determined by the
|
||||
front-end perspective on the proof document, while making
|
||||
adequate use of the CPU resources on multicore hardware on
|
||||
the back-end.
|
||||
|
||||
Recent refinements of Isabelle/PIDE provide an explicit
|
||||
concept of asynchronous print functions over existing proof
|
||||
states. This allows to integrate long-running or
|
||||
potentially non-terminating tools into the document-model.
|
||||
Applications range from traditional proof state output
|
||||
(which may consume substantial time in interactive
|
||||
development) to automated provers and dis-provers that
|
||||
report on existing proof document content (e.g.
|
||||
Sledgehammer, Nitpick, Quickcheck in Isabelle/HOL).
|
||||
Moreover, it is possible to integrate query operations via
|
||||
additional GUI panels with separate input and output (e.g.
|
||||
for Sledgehammer or find-theorems). Thus the Prover IDE
|
||||
provides continuous proof processing, augmented by add-on
|
||||
tools that help the user to continue writing proofs.
|
||||
}
|
||||
}
|
||||
|
||||
@Proceedings{ klein.ea:interactive:2014,
|
||||
editor = {Gerwin Klein and Ruben Gamboa},
|
||||
title = {Interactive Theorem Proving - 5th International
|
||||
Conference, {ITP} 2014, Held as Part of the Vienna Summer
|
||||
of Logic, {VSL} 2014, Vienna, Austria, July 14-17, 2014.
|
||||
Proceedings},
|
||||
series = s-lncs,
|
||||
volume = 8558,
|
||||
publisher = pub-springer,
|
||||
year = 2014,
|
||||
doi = {10.1007/978-3-319-08970-6},
|
||||
isbn = {978-3-319-08969-0}
|
||||
}
|
||||
|
||||
@InProceedings{ bezzecchi.ea:making:2018,
|
||||
title = {Making Agile Development Processes fit for V-style
|
||||
Certification Procedures},
|
||||
author = {Bezzecchi, S. and Crisafulli, P. and Pichot, C. and Wolff,
|
||||
B.},
|
||||
booktitle = {{ERTS'18}},
|
||||
abstract = {We present a process for the development of safety and
|
||||
security critical components in transportation systems
|
||||
targeting a high-level certification (CENELEC 50126/50128,
|
||||
DO 178, CC ISO/IEC 15408).
|
||||
|
||||
The process adheres to the objectives of an ``agile
|
||||
development'' in terms of evolutionary flexibility and
|
||||
continuous improvement. Yet, it enforces the overall
|
||||
coherence of the development artifacts (ranging from proofs
|
||||
over tests to code) by a particular environment (CVCE).
|
||||
|
||||
In particular, the validation process is built around a
|
||||
formal development based on the interactive theorem proving
|
||||
system Isabelle/HOL, by linking the business logic of the
|
||||
application to the operating system model, down to code and
|
||||
concrete hardware models thanks to a series of refinement
|
||||
proofs.
|
||||
|
||||
We apply both the process and its support in CVCE to a
|
||||
case-study that comprises a model of an odometric service
|
||||
in a railway-system with its corresponding implementation
|
||||
integrated in seL4 (a secure kernel for which a
|
||||
comprehensive Isabelle development exists). Novel
|
||||
techniques implemented in Isabelle enforce the coherence of
|
||||
semi-formal and formal definitions within to specific
|
||||
certification processes in order to improve their
|
||||
cost-effectiveness. },
|
||||
pdf = {https://www.lri.fr/~wolff/papers/conf/2018erts-agile-fm.pdf},
|
||||
year = 2018,
|
||||
series = {ERTS Conference Proceedings},
|
||||
location = {Toulouse}
|
||||
}
|
||||
|
||||
@MISC{owl2012,
|
||||
title = {OWL 2 Web Ontology Language},
|
||||
note={\url{https://www.w3.org/TR/owl2-overview/}, Document Overview (Second Edition)},
|
||||
author = {World Wide Web Consortium}
|
||||
}
|
||||
|
||||
|
||||
@MISC{ protege,
|
||||
title = {Prot{\'e}g{\'e}},
|
||||
note={\url{https://protege.stanford.edu}},
|
||||
year = {2018}
|
||||
}
|
||||
|
||||
@MISC{ cognitum,
|
||||
title = {Fluent Editor},
|
||||
note={\url{http://www.cognitum.eu/Semantics/FluentEditor/}},
|
||||
year = {2018}
|
||||
}
|
||||
|
||||
@MISC{ neon,
|
||||
title = {The NeOn Toolkit},
|
||||
note = {\url{http://neon-toolkit.org}},
|
||||
year = {2018}
|
||||
}
|
||||
|
||||
@MISC{ owlgred,
|
||||
title = {OWLGrEd},
|
||||
note={\url{http://owlgred.lumii.lv/}},
|
||||
year = {2018}
|
||||
}
|
||||
|
||||
@MISC{ rontorium,
|
||||
title = {R Language Package for FLuent Editor (rOntorion)},
|
||||
note={\url{http://www.cognitum.eu/semantics/FluentEditor/rOntorionFE.aspx}},
|
||||
year = {2018}
|
||||
}
|
||||
|
|
@ -0,0 +1,83 @@
|
|||
%% Copyright (C) 2018 The University of Sheffield
|
||||
%% 2018 The University of Paris-Sud
|
||||
%%
|
||||
%% License:
|
||||
%% This program can be redistributed and/or modified under the terms
|
||||
%% of the LaTeX Project Public License Distributed from CTAN
|
||||
%% archives in directory macros/latex/base/lppl.txt; either
|
||||
%% version 1 of the License, or any later version.
|
||||
%% OR
|
||||
%% The 2-clause BSD-style license.
|
||||
%%
|
||||
%% SPDX-License-Identifier: LPPL-1
|
||||
|
||||
%% Warning: Do Not Edit!
|
||||
%% =====================
|
||||
%% This is the root file for the Isabelle/DOF.
|
||||
%% All customization and/or additional packages should be added to the file
|
||||
%% preamble.tex.
|
||||
|
||||
|
||||
\RequirePackage{ifvtex}
|
||||
\documentclass[fontsize=11pt,DIV12,paper=a4]{scrartcl}
|
||||
\usepackage[T1]{fontenc}
|
||||
\usepackage[utf8]{inputenc}
|
||||
\usepackage{textcomp}
|
||||
\usepackage[english]{babel}
|
||||
\usepackage{isabelle}
|
||||
\input{ontologies}
|
||||
\IfFileExists{preamble.tex}{\input{preamble.tex}}{}%
|
||||
\usepackage{isabellesym}
|
||||
\usepackage{amsmath}
|
||||
\usepackage{amssymb}
|
||||
\usepackage[numbers, sort&compress, sectionbib]{natbib}
|
||||
|
||||
\usepackage{graphicx}
|
||||
\usepackage[caption]{subfig}
|
||||
\usepackage[size=footnotesize]{caption}
|
||||
|
||||
\newcommand{\ie}{i.e.}
|
||||
\newcommand{\eg}{e.g.}
|
||||
|
||||
|
||||
\usepackage{hyperref}
|
||||
\setcounter{tocdepth}{3}
|
||||
\hypersetup{%
|
||||
bookmarksdepth=3
|
||||
,pdfpagelabels
|
||||
,pageanchor=true
|
||||
,bookmarksnumbered
|
||||
,plainpages=false
|
||||
} % more detailed digital TOC (aka bookmarks)
|
||||
\sloppy
|
||||
\allowdisplaybreaks[4]
|
||||
\urlstyle{rm}
|
||||
\isabellestyle{it}
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
%%% Overrides the (rightfully issued) warning by Koma Script that \rm
|
||||
%%% etc. should not be used (they are deprecated since more than a
|
||||
%%% decade)
|
||||
\DeclareOldFontCommand{\rm}{\normalfont\rmfamily}{\mathrm}
|
||||
\DeclareOldFontCommand{\sf}{\normalfont\sffamily}{\mathsf}
|
||||
\DeclareOldFontCommand{\tt}{\normalfont\ttfamily}{\mathtt}
|
||||
\DeclareOldFontCommand{\bf}{\normalfont\bfseries}{\mathbf}
|
||||
\DeclareOldFontCommand{\it}{\normalfont\itshape}{\mathit}
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
|
||||
\title{<TITLE>}
|
||||
\author{<AUTHOR>}
|
||||
\begin{document}
|
||||
\maketitle
|
||||
\input{session}
|
||||
% optional bibliography
|
||||
\IfFileExists{root.bib}{%
|
||||
\bibliographystyle{abbrvnat}
|
||||
\bibliography{root}
|
||||
}{}
|
||||
\end{document}
|
||||
|
||||
%%% Local Variables:
|
||||
%%% mode: latex
|
||||
%%% TeX-master: t
|
||||
%%% End:
|