forked from Isabelle_DOF/Isabelle_DOF
steps to reform cicm/csp paper and manual
This commit is contained in:
parent
dc7ed74c57
commit
7f4b587274
|
@ -1,3 +1,4 @@
|
|||
scholarly_paper
|
||||
technical_report
|
||||
math_exam
|
||||
CENELEC_50128
|
||||
|
|
|
@ -16,12 +16,9 @@ setup \<open> DOF_lib.define_shortcut \<^binding>\<open>csp\<close> "CSP
|
|||
|
||||
title*[tit::title]\<open>Philosophers may Dine - Definitively!\<close>
|
||||
|
||||
author*[safouan, email="''safouan.taha@lri.fr''",affiliation="\<open>LRI, CentraleSupelec\<close>"]
|
||||
\<open>Safouan Taha\<close>
|
||||
author*[bu, email= "''wolff@lri.fr''",affiliation = "\<open>LRI, Université Paris-Saclay\<close>"]
|
||||
\<open>Burkhart Wolff\<close>
|
||||
author*[lina,email="''lina.ye@lri.fr''",affiliation="\<open>LRI, Inria, LSV, CentraleSupelec\<close>"]
|
||||
\<open>Lina Ye\<close>
|
||||
author*[safouan,email="\<open>safouan.taha@lri.fr\<close>",affiliation="\<open>LRI, CentraleSupelec\<close>"]\<open>Safouan Taha\<close>
|
||||
author*[bu,email= "\<open>wolff@lri.fr\<close>",affiliation = "\<open>LRI, Université Paris-Saclay\<close>"]\<open>Burkhart Wolff\<close>
|
||||
author*[lina,email="\<open>lina.ye@lri.fr\<close>",affiliation="\<open>LRI, Inria, LSV, CentraleSupelec\<close>"]\<open>Lina Ye\<close>
|
||||
|
||||
abstract*[abs, keywordlist="[\<open>Shallow Embedding\<close>,\<open>Process-Algebra\<close>,
|
||||
\<open>Concurrency\<close>,\<open>Computational Models\<close>]"]
|
||||
|
|
|
@ -100,47 +100,46 @@ open_monitor*[this::report]
|
|||
|
||||
(*>*)
|
||||
|
||||
title*[title::title]\<open>Isabelle/DOF\<close>
|
||||
title*[title::title] \<open>Isabelle/DOF\<close>
|
||||
subtitle*[subtitle::subtitle]\<open>User and Implementation Manual\<close>
|
||||
text*[adb:: author,
|
||||
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>
|
||||
text*[bu::author,
|
||||
email = "\<open>wolff@lri.fr\<close>",
|
||||
affiliation = "\<open>Université Paris-Saclay, LRI, Paris, France\<close>"]\<open>Burkhart Wolff\<close>
|
||||
author*[ adb,
|
||||
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>
|
||||
author*[ bu,
|
||||
email = "\<open>wolff@lri.fr\<close>",
|
||||
affiliation = "\<open>Université Paris-Saclay, LRI, Paris, France\<close>"]\<open>Burkhart Wolff\<close>
|
||||
|
||||
text*[abs::abstract,
|
||||
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. \<^isadof> targets use-cases such as mathematical texts referring
|
||||
to a theory development or technical reports requiring a particular structure.
|
||||
A major application of \<^dof> is the integrated development of
|
||||
formal certification documents (\<^eg>, for Common Criteria or CENELEC
|
||||
50128) that require consistency across both formal and informal
|
||||
arguments.
|
||||
abstract*[abs, keywordlist="[\<open>Ontology\<close>, \<open>Ontological Modeling\<close>, \<open>Document Management\<close>,
|
||||
\<open>Formal Document Development\<close>,\<open>Document Authoring\<close>,\<open>Isabelle/DOF\<close>]"]
|
||||
\<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. \<^isadof> targets use-cases such as mathematical texts referring
|
||||
to a theory development or technical reports requiring a particular structure.
|
||||
A major application of \<^dof> is the integrated development of
|
||||
formal certification documents (\<^eg>, for Common Criteria or CENELEC
|
||||
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.
|
||||
Its checking facilities leverage the collaborative
|
||||
development of documents required to be consistent with an
|
||||
underlying ontological structure.
|
||||
\<^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.
|
||||
Its checking facilities leverage the collaborative
|
||||
development of documents required to be consistent with an
|
||||
underlying ontological structure.
|
||||
|
||||
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.
|
||||
|
||||
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.
|
||||
|
||||
It is an unique feature of \<^isadof> that ontologies may be used to control
|
||||
the link between formal and informal content in documents in a machine
|
||||
checked way. These links can connect both text elements as well as formal
|
||||
modelling elements such as terms, definitions, code and logical formulas,
|
||||
alltogether *\<open>integrated\<close> in a state-of-the-art interactive theorem prover.
|
||||
It is an unique feature of \<^isadof> that ontologies may be used to control
|
||||
the link between formal and informal content in documents in a machine
|
||||
checked way. These links can connect both text elements as well as formal
|
||||
modelling elements such as terms, definitions, code and logical formulas,
|
||||
alltogether *\<open>integrated\<close> in a state-of-the-art interactive theorem prover.
|
||||
\<close>
|
||||
|
||||
(*<*)
|
||||
|
|
BIN
examples/technical_report/Isabelle_DOF-Manual/document/figures/header_CSP_source.png
Executable file → Normal file
BIN
examples/technical_report/Isabelle_DOF-Manual/document/figures/header_CSP_source.png
Executable file → Normal file
Binary file not shown.
Before Width: | Height: | Size: 419 KiB After Width: | Height: | Size: 383 KiB |
Loading…
Reference in New Issue