Draft of Conclusion

examples/scholarly_paper/2021-ITP-PMTI/document/root.bib

@@ -37,6 +37,45 @@
 }
 
 
+@MISC{owl2012,
+   title = {OWL 2 Web Ontology Language},
+   note={\url{https://www.w3.org/TR/owl2-overview/}, Document Overview (Second Edition)},
+   author = {World Wide Web Consortium}
+}
+    
+
+@MISC{protege,
+  title = {Prot{\'e}g{\'e}},
+  note={\url{https://protege.stanford.edu}},
+  year = {2018}
+}
+
+@article{Nevzorova2014OntoMathPO,
+  title={OntoMath PRO Ontology: A Linked Data Hub for Mathematics},
+  author={Olga Nevzorova and Nikita Zhiltsov and Alexander Kirillovich and Evgeny Konstantinovich Lipachev},
+  journal={ArXiv},
+  pdf = {\url{https://kpfu.ru/staff_files/F_438204284/OntoMathPro_ontology_KESW2014.pdf}},
+  doi = {10.1007/978-3-319-11716-4_9},
+  year={2014},
+  volume={abs/1407.4833}
+}
+
+@InProceedings{10.1007/978-3-030-79876-5_6,
+author="Nipkow, Tobias
+and Ro{\ss}kopf, Simon",
+editor="Platzer, Andr{\'e}
+and Sutcliffe, Geoff",
+title="Isabelle's Metalogic: Formalization and Proof Checker",
+booktitle="Automated Deduction -- CADE 28",
+year="2021",
+publisher="Springer International Publishing",
+address="Cham",
+pages="93--110",
+abstract="Isabelle is a generic theorem prover with a fragment of higher-order logic as a metalogic for defining object logics. Isabelle also provides proof terms. We formalize this metalogic and the language of proof terms in Isabelle/HOL, define an executable (but inefficient) proof term checker and prove its correctness w.r.t. the metalogic. We integrate the proof checker with Isabelle and run it on a range of logics and theories to check the correctness of all the proofs in those theories.",
+isbn="978-3-030-79876-5"
+}
+
+
 @TechReport{Parsia:12:OWO,
   author      = "Bijan Parsia and Boris Motik and Peter Patel-Schneider",
   title       = "{OWL} 2 Web Ontology Language Structural Specification and Functional-Style Syntax (Second Edition)",