Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

added elements to related work: OntoMathPro, ScienceWISE, DBpedia

This commit is contained in:
Burkhart Wolff 2022-01-20 22:08:32 +01:00
parent 688e823463
commit d7c7a98138
2 changed files with 65 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

31
examples/scholarly_paper/2021-ITP-PMTI/document/root.bib
View File

@ -259,6 +259,37 @@ isbn="978-3-540-48509-4"
year = {2006}
}
@InProceedings{10.1007/978-3-540-76298-0_52,
author="Auer, S{\"o}ren
and Bizer, Christian
and Kobilarov, Georgi
and Lehmann, Jens
and Cyganiak, Richard
and Ives, Zachary",
editor="Aberer, Karl
and Choi, Key-Sun
and Noy, Natasha
and Allemang, Dean
and Lee, Kyung-Il
and Nixon, Lyndon
and Golbeck, Jennifer
and Mika, Peter
and Maynard, Diana
and Mizoguchi, Riichiro
and Schreiber, Guus
and Cudr{\'e}-Mauroux, Philippe",
title="DBpedia: A Nucleus for a Web of Open Data",
booktitle="The Semantic Web",
year="2007",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="722--735",
abstract="DBpedia is a community effort to extract structured information from Wikipedia and to make this information available on the Web. DBpedia allows you to ask sophisticated queries against datasets derived from Wikipedia and to link other datasets on the Web to Wikipedia data. We describe the extraction of the DBpedia datasets, and how the resulting information is published on the Web for human- and machine-consumption. We describe some emerging applications from the DBpedia community and show how website authors can facilitate DBpedia content within their sites. Finally, we present the current status of interlinking DBpedia with other open datasets on the Web and outline how DBpedia could serve as a nucleus for an emerging Web of open data.",
isbn="978-3-540-76298-0"
}
@InProceedings{ thomas:role-based:1996,
author = {Roshan Thomas},
title = {Role-based access control and distributed object-based

39
examples/scholarly_paper/2021-ITP-PMTI/paper.thy
View File

@ -33,8 +33,8 @@ abstract*[abs, keywordlist="[\<open>Ontologies\<close>,\<open>Formal Documents\<
\<^dof> allows for the formal development of ontologies as well as continuous checking that
a formal document under development conforms to an underlying ontology.
Such a document may contain text and code elements as well as formal Isabelle definitions and proofs.
Thus, \<^dof> is designed to annotate and interact with these elements with typed meta-data
for, \<^eg>, formal text development in Isabelle.
Thus, \<^dof> is designed to annotate and interact with typed meta-data
within formal developments in Isabelle.
While prior versions of \<^dof> provided already a mechanism to check ontological \<^emph>\<open>rules\<close>
(in OWL terminology) or \<^emph>\<open>class invariants\<close> (in UML/OCL terminology) via hand-written SML test-code,
@ -125,10 +125,8 @@ Isabelle community for a deeper structuring of the Archive of Formal Proofs (AFP
declare_reference*[casestudy::text_section]
(*>*)
section\<open>Background\<close>
subsection\<open>Isabelle/DOF Design and Implementation\<close>
section*[bgrnd::text_section,main_author="Some(@{docitem ''adb''}::author)"] \<open> Background\<close>
subsection\<open>Isabelle/DOF Design and Implementation\<close>
text\<open>
In this section, we provide a guided tour through the underlying technologies of this paper:
\begin{inparaenum}
@ -289,6 +287,8 @@ text\<open>
\<^item> \<^url>\<open>https://www.una.edu/writingcenter/docs/Writing-Resources/Source%20Integration.pdf\<close>
\<^item> \<^url>\<open>https://www.exoscale.com/syslog/what-is-continuous-integration/\<close>
\<close>
(*
Data integration driven ontology design, case study smart city
@ -298,6 +298,35 @@ WIMS '13: Proceedings of the 3rd International Conference on Web Intelligence,
https://doi.org/10.1145/2479787.2479830
*)
section\<open> Related work \<close>
text\<open>
\<^item> Geschwalle: Tom Gruber's "Ontology for Engineering Mathematics"
\<^url>\<open>https://tomgruber.org/writing/an-ontology-for-engineering-mathematics\<close>
\<^item> OntoMathPro contains indeed something like a "taxonomy of the fields of mathematics" pp 110
\<^url>\<open>https://kpfu.ru/staff_files/F_438204284/OntoMathPro_ontology_KESW2014.pdf\<close>
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>\<open>http://www.edu.ru/db-mon/mo/Data/d_10/prm40-1.pdf\<close>
\<^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>\<open>http://dbpedia.org/sparql\<close>
\<^item> Other Onto: ScienceWISE
\<^url>\<open>http://data.sciencewise.info/openrdf-sesame/repositories/SW\<close>
\<^url>\<open>https://github.com/CLLKazan/OntoMathPro\<close>
\<^item> Search Engines: Wikipedia Formula Search, \<^url>\<open>http://shinh.org/wfs\<close>
\<close>
section\<open>Annex\<close>
subsection\<open>Remotely relevant stuff\<close>