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
|
|
|
|
|
evolution. A major goal of \dof is the integrated development of
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
In this paper, we give an in-depth presentation of the design
|
|
|
|
|
concepts of \dof's Ontology Definition Language (ODL) and key
|
|
|
|
|
aspects of the technology of its implementation. \isadof is the
|
|
|
|
|
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
|
|
|
|
|
(*>*)
|
|
|
|
|
|
