diff --git a/examples/scholarly_paper/2021-ITP-PMTI/document/root.bib b/examples/scholarly_paper/2021-ITP-PMTI/document/root.bib index 24b840e..1bced51 100644 --- a/examples/scholarly_paper/2021-ITP-PMTI/document/root.bib +++ b/examples/scholarly_paper/2021-ITP-PMTI/document/root.bib @@ -57,21 +57,31 @@ year = {1995} } -@TechReport{owl2012, - author = "", - title = "{OWL} 2 Web Ontology Language Document Overview (Second Edition)", - month = dec, - note = "https://www.w3.org/TR/2012/REC-owl2-overview-20121211/", - year = "2012", - bibsource = "https://w2.syronex.com/jmr/w3c-biblio", - type = "", - institution = "W3C", +@incollection{OWL2014, + author = {Kunal Sengupta and + Pascal Hitzler}, + title = {Web Ontology Language {(OWL)}}, + booktitle = {Encyclopedia of Social Network Analysis and Mining}, + pages = {2374--2378}, + year = {2014}, + doi = {10.1007/978-1-4614-6170-8\_113} } -@MISC{protege, - title = {Prot{\'e}g{\'e}}, - note={\url{https://protege.stanford.edu}}, - year = {2018} +@article{protege, +author = {Musen, Mark A.}, +title = {The Prot\'{e}G\'{e} Project: A Look Back and a Look Forward}, +year = {2015}, +issue_date = {June 2015}, +publisher = {Association for Computing Machinery}, +address = {New York, NY, USA}, +volume = {1}, +number = {4}, +url = {https://doi.org/10.1145/2757001.2757003}, +doi = {10.1145/2757001.2757003}, +journal = {AI Matters}, +month = {jun}, +pages = {4–12}, +numpages = {9} } @article{Nevzorova2014OntoMathPO, diff --git a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy index a4eb3a0..912624d 100644 --- a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy +++ b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy @@ -233,7 +233,7 @@ text\As novel contribution, this work extends prior versions of \<^dof> by (rather than SML code or semi-formal text). Thus, annotations generated from \<^dof> may also occur in \\\-terms used to denote meta-data. \<^enum> formal, machine-checked invariants on meta-data, which correspond to the concept of - ``rules'' in OWL~ @{cite "owl2012"} or ``constraints'' in UML, and which can be specified in + ``rules'' in OWL~ @{cite "OWL2014"} or ``constraints'' in UML, and which can be specified in common \<^hol> \\\-term syntax. \ text\ For example, the \<^dof> evaluation command taking a \<^hol>-expression: @@ -1280,7 +1280,7 @@ Our experiments with adaptions of existing ontologies from engineering and mathe show that \<^dof>'s ODL has sufficient expressive power to cover all aspects of languages such as OWL (with perhaps the exception of multiple inheritance on classes). However, these ontologies have been developed specifically \<^emph>\in\ OWL and target -its specific support, the Protege editor @{cite "protege"}. We argue that \<^dof> might ask +its specific support, the Protégé editor @{cite "protege"}. We argue that \<^dof> might ask for a re-engineering of these ontologies: less deep hierarchies, rather deeper structure in meta-data and stronger invariants. \ @@ -1314,13 +1314,13 @@ information and knowledge, and to make it amenable to OntoMath\textsuperscript{PRO} contains the daunting number of 3,449 classes, which is in part due to the need to compensate the lack of general datatype definition methods for meta-data. It is inspired from a translation of the Russian Federal Standard for Higher Education - on mathematics for master students \<^url>\http://www.edu.ru/db-mon/mo/Data/d_10/prm40-1.pdf\, + on mathematics for master students, which makes it nevertheless an interesting starting point for a future development of a mathematics ontology in the \<^dof> framework. \<^item> Other ontologies worth mentioning are DBpedia @{cite "10.1007/978-3-540-76298-0_52"}, which provides with the \<^emph>\SPARQL endpoint\ \<^url>\http://dbpedia.org/sparql\ a search engine, - and the more general ScienceWISE (see \<^url>\http://sciencewise.info/ontology/\ linked to the - ArXiv.org project) that allows users to introduce their own category concepts. + and the more general ScienceWISE \<^footnote>\\<^url>\http://sciencewise.info/ontology/\.\ + that allows users to introduce their own category concepts. Both suffer from the lack of deeper meta-data modeling, and the latter is still at the beginning (ScienceWISE marks the Mathematics part as ``under construction''). @@ -1336,8 +1336,8 @@ information and knowledge, and to make it amenable to subsection*[fw::related_work]\Future Work\ text\ We plan to complement \<^dof> with incremental LaTeX generation and a previewing facility that will further increase the usability of our framework for the ontology-conform editing -of formal content, be it in the engineering or the mathematics domain. -\<^footnote>\This paper has been edited in \<^dof>, of course.\ +of formal content, be it in the engineering or the mathematics domain +(this paper has been edited in \<^dof>, of course). Another line of future application is to increase the ``depth'' of built-in term antiquotations such as \<^theory_text>\@{typ \'\\}\, \<^theory_text>\@{term \a + b\}\ and \<^theory_text>\@{thm \HOL.refl\}\, which are currently implemented