2019-08-15 14:09:55 +00:00
|
|
|
(*************************************************************************
|
|
|
|
* Copyright (C)
|
|
|
|
* 2019 The University of Exeter
|
|
|
|
* 2018-2019 The University of Paris-Saclay
|
|
|
|
* 2018 The University of Sheffield
|
|
|
|
*
|
|
|
|
* License:
|
|
|
|
* This program can be redistributed and/or modified under the terms
|
|
|
|
* of the 2-clause BSD-style license.
|
|
|
|
*
|
|
|
|
* SPDX-License-Identifier: BSD-2-Clause
|
|
|
|
*************************************************************************)
|
|
|
|
|
2018-12-04 05:31:45 +00:00
|
|
|
(*<*)
|
|
|
|
theory "00_Frontmatter"
|
2019-07-12 19:20:02 +00:00
|
|
|
imports "Isabelle_DOF.technical_report"
|
2018-12-04 05:31:45 +00:00
|
|
|
begin
|
|
|
|
|
2018-12-06 11:31:12 +00:00
|
|
|
open_monitor*[this::report]
|
2018-12-04 05:31:45 +00:00
|
|
|
|
|
|
|
(*>*)
|
|
|
|
|
2019-07-23 06:51:27 +00:00
|
|
|
title*[title::title]\<open>Isabelle/DOF\<close>
|
|
|
|
subtitle*[subtitle::subtitle]\<open>User and Implementation Manual\<close>
|
2018-12-04 05:31:45 +00:00
|
|
|
text*[adb:: author,
|
2019-07-21 15:14:42 +00:00
|
|
|
email="\<open>a.brucker@exeter.ac.uk\<close>",
|
|
|
|
orcid="\<open>0000-0002-6355-1200\<close>",
|
|
|
|
http_site="\<open>https://www.brucker.ch/\<close>",
|
|
|
|
affiliation="\<open>University of Exeter, Exeter, UK\<close>"]\<open>Achim D. Brucker\<close>
|
2018-12-04 05:31:45 +00:00
|
|
|
text*[bu::author,
|
2019-07-21 15:14:42 +00:00
|
|
|
email = "\<open>wolff@lri.fr\<close>",
|
|
|
|
affiliation = "\<open>Université Paris-Saclay, LRI, Paris, France\<close>"]\<open>Burkhart Wolff\<close>
|
|
|
|
|
2018-12-04 05:31:45 +00:00
|
|
|
text*[abs::abstract,
|
2019-07-30 21:57:22 +00:00
|
|
|
keywordlist="[''Ontology'', ''Ontological Modeling'', ''Document Management'',
|
|
|
|
''Formal Document Development'', ''Document Authoring'', ''Isabelle/DOF'']"]
|
|
|
|
\<open> \isadof provides an implementation of \dof on top of Isabelle/HOL.
|
|
|
|
\dof itself is a novel framework for \<^emph>\<open>defining\<close> ontologies
|
|
|
|
and \<^emph>\<open>enforcing\<close> them during document development and document
|
2019-08-17 08:23:16 +00:00
|
|
|
evolution. \isadof targets use-cases such as mathematical texts referring
|
|
|
|
to a theory development or technical reports requiring a particular structure.
|
|
|
|
A major application of \dof is the integrated development of
|
2019-07-30 21:57:22 +00:00
|
|
|
formal certification documents (\eg, for Common Criteria or CENELEC
|
|
|
|
50128) that require consistency across both formal and informal
|
|
|
|
arguments.
|
|
|
|
|
|
|
|
\isadof is integrated into Isabelle's IDE, which
|
|
|
|
allows for smooth ontology development as well as immediate
|
|
|
|
ontological feedback during the editing of a document.
|
2019-08-17 08:23:16 +00:00
|
|
|
Its checking facilities leverage the collaborative
|
|
|
|
development of documents required to be consistent with an
|
|
|
|
underlying ontological structure.
|
2019-07-30 21:57:22 +00:00
|
|
|
|
2019-08-17 08:23:16 +00:00
|
|
|
In this user-manual, we give an in-depth presentation of the design
|
|
|
|
concepts of \dof's Ontology Definition Language (ODL) and describe
|
|
|
|
comprehensively its major commands. Many examples show typical best-practice
|
|
|
|
applications of the system. \isadof is the
|
2019-07-30 21:57:22 +00:00
|
|
|
first ontology language supporting machine-checked
|
|
|
|
links between the formal and informal parts in an LCF-style
|
|
|
|
interactive theorem proving environment.
|
2018-12-04 05:31:45 +00:00
|
|
|
\<close>
|
|
|
|
|
|
|
|
(*<*)
|
|
|
|
end
|
|
|
|
(*>*)
|
|
|
|
|