diff --git a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy index 6e8a8fe3..3507e666 100644 --- a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy +++ b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy @@ -197,7 +197,8 @@ ITP community allowing a deeper structuring of mathematical libraries such as th declare_reference*[casestudy::text_section] (*>*) -section*[bgrnd::text_section,main_author="Some(@{docitem ''adb''}::author)"] \ Background\ +section*[bgrnd::background,main_author="Some(@{docitem ''bu''}::author)"] \ Background\ +(* subsection\Isabelle/DOF Design and Implementation\ text\ In this section, we provide a guided tour through the underlying technologies of this paper: @@ -215,32 +216,25 @@ text\ The plugin Isabelle/HOL offers a modeling language similar to functional programming languages extended by a logic and automated proof and animation techniques. \ - -subsection*[bgrnd_isadof::text_section]\The \<^dof> Framework\ +*) +subsection*[bgrnd_isadof::background]\The \<^dof> Framework\ text\ \<^dof> ~@{cite "brucker.ea:isabelle-ontologies:2018" and "brucker.ea:isabelledof:2019"} - is a document ontology framework that extends Isabelle/HOL. We understand - by a \<^emph>\document ontology\ structured meta-data attached to an integrated document allowing - classifying text-elements, connect them to typed meta-data, and establishing typed links between text- - and formal elements (such as definitions, proofs, code, test-results, etc). - + is a document ontology framework that extends Isabelle/HOL. \<^dof> offers basically two things: a language called ODL to \<^emph>\specify\ a formal ontology, and ways to \<^emph>\annotate\ an integrated document written in Isabelle/HOL with the specified - meta-data. Additionally, \<^dof> generates from an ontology a family of semantic macros---called - \<^emph>\antiquotations\ that may appear in text or code---allowing establishing - machine-checked links between classified entities. Not unlike the UML/OCL meta-model, ODL offers class - invariants as well as means to express - structural constraints in documents. - Unlike UML, however, \<^dof> allows for integrated documents with informal and formal elements - including the necessary management of logical contexts. + meta-data. Additionally, \<^dof> generates from an ontology a family of + \<^emph>\antiquotations\ allowing to establish machine-checked links between classified entities. +% Unlike UML, however, \<^dof> allows for integrated documents with informal and formal elements +% including the necessary management of logical contexts. The perhaps most attractive aspect of \<^dof> is its deep integration into the IDE of Isabelle - (PIDE), which allows hypertext-like navigation as well as fast user-feedback - during development and evolution of the integrated document. This includes rich editing support, + (PIDE), which allows a hypertext-like navigation as well as fast user-feedback + during development and evolution of the integrated source. This includes rich editing support, including on-the-fly semantics checks, hinting, or auto-completion. \<^dof> supports \<^LaTeX> - based document generation as well as ontology-aware ``views'' on - the integrated document, \ie, specific versions of generated PDF addressing, + the integrated document, \<^ie>, specific versions of generated PDF addressing, for example, different stake-holders. \ @@ -248,7 +242,7 @@ text\ figure*[isadof_screenshot::figure, relative_width="100", src="''figures/cicm2018-combined''"]\ The \<^dof> IDE (left) and the corresponding PDF(right). \ -text*[description_scrrenshot::text_section]\ +text*[description_scrrenshot::background]\ @{docitem \isadof_screenshot\} shows \<^dof> in action: the left-hand side shows the IDE of \<^dof> in the context of a user session maintaining our case study (see @{docitem (unchecked) "casestudy"}) @@ -257,7 +251,7 @@ text*[description_scrrenshot::text_section]\ \ (*>*) -subsection*[bgrnd_ODL::text_section]\A Guided Tour through ODL\ +subsection*[bgrnd_ODL::background]\A Guided Tour through ODL\ text\ \<^dof> provides a strongly typed Ontology Definition Language (ODL) that provides the usual concepts of ontologies such as @@ -300,6 +294,8 @@ text\\autoref{text-elements} shows an ontological annotation of a requirem it suffices to click on its keyword: the IDE will display the class-definition and its surrounding documentation in the ontology.\ +(* + text\\<^dof>'s generated antiquotations are part of a general mechanism of Isabelle's standard antiquotations heavily used in various papers and technical reports. For example, in the following informal text, the antiquotation \<^verbatim>\thm refl\ refers @@ -323,15 +319,18 @@ text\\<^dof>'s generated antiquotations are part of a general mechanism of generated glossaries or lists of concepts. \ +*) + +subsection\Meta-Objects as Extensible Records\ + +text\Explain record notation.\ subsection\Code-Generation in Isabelle\ text\Explain eval and nbe, and refer to references.\ - - - -section\Invariants in DOF\ +section*[invariants::technical,main_author="Some(@{docitem ''nic''}::author)"] +\Term-Context support and Invariants in DOF\ text\ A novel mechanism to specify invariants is implemented @@ -410,10 +409,9 @@ datatype kind = expert_opinion | argument | "proof" when the instance \<^emph>\testinv2\ is defined. \ +subsection\Example and Queries\ -section\Proving Morphisms on Ontologies\ - -section\Example and Queries\ +section*["morphisms"::technical,main_author="Some(@{docitem ''idir''}::author)"] \Proving Morphisms on Ontologies\ text\ A new mechanism to make query on instances is available and uses the HOL implementation of Lists. @@ -448,8 +446,34 @@ subsection\Engineering Example : An Extract from PLib\ subsection\Mathematics Example : An Extract from OntoMathPro\ -section\Conclusion\ -subsection\Related Works\ +section*[concl::conclusion]\Conclusion\ +subsection*[rw::related_work]\Related Works\ + +text\ +\<^item> Geschwalle: Tom Gruber's "Ontology for Engineering Mathematics" + \<^url>\https://tomgruber.org/writing/an-ontology-for-engineering-mathematics\ +\<^item> OntoMathPro contains indeed something like a "taxonomy of the fields of mathematics" pp 110 + \<^url>\https://kpfu.ru/staff_files/F_438204284/OntoMathPro_ontology_KESW2014.pdf\ + According to In total, OntoMathPRO contains 3,449 classes ... + +\<^item> Translated from the Russian Federal Standard for Higher Education on mathematics + for master students, Section 5.2: + \<^url>\http://www.edu.ru/db-mon/mo/Data/d_10/prm40-1.pdf\ +\<^item> Elements of OntoMathPro : + (* figures/OntoMathPro-Taxonomy.png + figures/OntoMathPro-Taxonomy-2.png *) +\<^item> Other Onto: DBpedia @{cite "10.1007/978-3-540-76298-0_52"} + SPARQL endpoint: \<^url>\http://dbpedia.org/sparql\ +\<^item> Other Onto: ScienceWISE + \<^url>\http://data.sciencewise.info/openrdf-sesame/repositories/SW\ + \<^url>\https://github.com/CLLKazan/OntoMathPro\ + +\<^item> Search Engines: Wikipedia Formula Search, \<^url>\http://shinh.org/wfs\ + +\<^item> And then: The stuff from Univ Erlangen (Kohlhase et al). + +\ + subsubsection\The notion of \<^emph>\Integrated Source\\ text\Links to the term: Integrated Document \<^item> \<^url>\https://www.openkm.com/blog/integrated-document-management.html\ @@ -485,34 +509,8 @@ https://doi.org/10.1145/2479787.2479830 *) -section\ Related work \ - -text\ -\<^item> Geschwalle: Tom Gruber's "Ontology for Engineering Mathematics" - \<^url>\https://tomgruber.org/writing/an-ontology-for-engineering-mathematics\ -\<^item> OntoMathPro contains indeed something like a "taxonomy of the fields of mathematics" pp 110 - \<^url>\https://kpfu.ru/staff_files/F_438204284/OntoMathPro_ontology_KESW2014.pdf\ - According to In total, OntoMathPRO contains 3,449 classes ... - -\<^item> Translated from the Russian Federal Standard for Higher Education on mathematics - for master students, Section 5.2: - \<^url>\http://www.edu.ru/db-mon/mo/Data/d_10/prm40-1.pdf\ -\<^item> Elements of OntoMathPro : - (* figures/OntoMathPro-Taxonomy.png - figures/OntoMathPro-Taxonomy-2.png *) -\<^item> Other Onto: DBpedia @{cite "10.1007/978-3-540-76298-0_52"} - SPARQL endpoint: \<^url>\http://dbpedia.org/sparql\ -\<^item> Other Onto: ScienceWISE - \<^url>\http://data.sciencewise.info/openrdf-sesame/repositories/SW\ - \<^url>\https://github.com/CLLKazan/OntoMathPro\ - -\<^item> Search Engines: Wikipedia Formula Search, \<^url>\http://shinh.org/wfs\ - -\<^item> And then: The stuff from Univ Erlangen (Kohlhase et al). - -\ - +text\\pagebreak\ section\Annex\ subsection\Remotely relevant stuff\