diff --git a/examples/scholarly_paper/2021-ITP-PMTI/document/root.bib b/examples/scholarly_paper/2021-ITP-PMTI/document/root.bib index f3f9b1f2..b288603a 100644 --- a/examples/scholarly_paper/2021-ITP-PMTI/document/root.bib +++ b/examples/scholarly_paper/2021-ITP-PMTI/document/root.bib @@ -389,7 +389,7 @@ and Maynard, Diana and Mizoguchi, Riichiro and Schreiber, Guus and Cudr{\'e}-Mauroux, Philippe", -title="DBpedia: A Nucleus for a Web of Open Data", +title="{DB}pedia: A Nucleus for a Web of Open Data", booktitle="The Semantic Web", year="2007", publisher="Springer Berlin Heidelberg", diff --git a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy index 062891cd..a7e0e21b 100644 --- a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy +++ b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy @@ -586,7 +586,7 @@ text*[introduction2::myintroduction, authored_by = "{@{myauthor \church\\ \} -\caption{Some instances of the classes of the ontology in the \autoref{fig-ontology-example}.} +\caption{Some instances of the classes of the ontology of \autoref{fig-ontology-example}.} \label{fig-instances-example} \end{figure} In the instance \<^theory_text>\introduction1\, the term antiquotation \<^theory_text>\@{myauthor \church\}\, @@ -1047,7 +1047,7 @@ onto_class assoc_Method_Problem = (*>*) text\ - The ontology \<^emph>\OntoMath\textsuperscript{PRO}\ @{cite "Nevzorova2014OntoMathPO"} + The \<^emph>\OntoMath\textsuperscript{PRO}\ ontology~@{cite "Nevzorova2014OntoMathPO"} is an OWL ontology of mathematical knowledge concepts. It posits the IS-A semantics for hierarchies of mathematical knowledge elements, and defines these elements as two hierarchies of classes: @@ -1057,9 +1057,10 @@ text\ like \<^const>\belongs_to\, \<^const>\contains\, \<^const>\defines\, \<^const>\is_defined_by\, \<^const>\solves\, \<^const>\is_solved_by\, and a symmetric transitive associative relation \<^const>\see_also\ between two mathematical knowledge objects. - It also represents links with external resources such as DBpedia - with annotations properties @{cite "Parsia:12:OWO"}. - \<^dof> covers a wide range of the OWL concepts used by the ontology OntoMath\textsuperscript{PRO}. + It also represents links with external resources + such as DBpedia~@{cite "10.1007/978-3-540-76298-0_52"} + with annotations properties~@{cite "Parsia:12:OWO"}. + \<^dof> covers a wide range of the OWL concepts used by the OntoMath\textsuperscript{PRO} ontology. We can represent the annotations properties as datatypes and then attach them as an attributes list to a class. For example the declaration: @@ -1088,7 +1089,7 @@ onto_class Field_of_mathematics = Here the \<^theory_text>\invariant restrict_annotation_F\ forces the \<^typ>\annotation\s to be a \<^const>\label\ or a \<^const>\comment\. Subsumption relation is straightforward. - The ontology OntoMath\textsuperscript{PRO} defines + The OntoMath\textsuperscript{PRO} ontology defines a \<^typ>\Problem\ and a \<^typ>\Method\ as subclasses of the class \<^typ>\Mathematical_knowledge_object\. It gives in \<^dof>: