{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T06:04:25Z","timestamp":1726034665472},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030232498"},{"type":"electronic","value":"9783030232504"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-23250-4_5","type":"book-chapter","created":{"date-parts":[[2019,7,2]],"date-time":"2019-07-02T03:01:17Z","timestamp":1562036477000},"page":"61-76","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Relational Data Across Mathematical Libraries"],"prefix":"10.1007","author":[{"given":"Andrea","family":"Condoluci","sequence":"first","affiliation":[]},{"given":"Michael","family":"Kohlhase","sequence":"additional","affiliation":[]},{"given":"Dennis","family":"M\u00fcller","sequence":"additional","affiliation":[]},{"given":"Florian","family":"Rabe","sequence":"additional","affiliation":[]},{"given":"Claudio","family":"Sacerdoti Coen","sequence":"additional","affiliation":[]},{"given":"Makarius","family":"Wenzel","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,7,3]]},"reference":[{"key":"5_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-642-45221-5_4","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"D Aspinall","year":"2013","unstructured":"Aspinall, D., Denney, E., L\u00fcth, C.: A semantic basis for proof queries and transformations. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 53\u201370. Springer, Heidelberg (2013). \n                    https:\/\/doi.org\/10.1007\/978-3-642-45221-5_4"},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-540-27818-4_2","volume-title":"Mathematical Knowledge Management","author":"A Asperti","year":"2004","unstructured":"Asperti, A., Selmi, M.: Efficient retrieval of mathematical statements. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol. 3119, pp. 17\u201331. Springer, Heidelberg (2004). \n                    https:\/\/doi.org\/10.1007\/978-3-540-27818-4_2"},{"key":"5_CR3","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/11617990_2","volume-title":"TYPES 2004","author":"A Asperti","year":"2006","unstructured":"Asperti, A., Guidi, F., Sacerdoti Coen, C., Tassi, E., Zacchiroli, S.: A content based mathematical search engine: whelp. In: Filli\u00e2tre, J.-C., Paulin-Mohring, C., Werner, B. (eds.) TYPES 2004. LNCS, vol. 3839, pp. 17\u201332. Springer, Heidelberg (2006). \n                    https:\/\/doi.org\/10.1007\/11617990_2"},{"issue":"4","key":"5_CR4","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/s11786-016-0274-0","volume":"10","author":"F Guidi","year":"2016","unstructured":"Guidi, F., Coen, C.S.: A survey on retrieval of mathematical knowledge. Math. Comput. Sci. 10(4), 409\u2013427 (2016). \n                    https:\/\/doi.org\/10.1007\/s11786-016-0274-0","journal-title":"Math. Comput. Sci."},{"key":"5_CR5","unstructured":"Lange, C.: Enabling Collaboration on Semiformal Mathematical Knowledge by Semantic Web Integration. Studies on the Semantic Web 11. AKA Verlag and IOS Press, Heidelberg and Amsterdam (2011)"},{"key":"5_CR6","unstructured":"Motik, B., Parsia, B., Patel-Schneider, P.F.: OWL 2 Web Ontology Language: XML Serialization. W3C Recommendation. World Wide Web Consortium (W3C), 27 October 2009. \n                    http:\/\/www.w3.org\/TR\/2009\/REC-owl2-xml-serialization-20091027\/"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-319-62075-6_7","volume-title":"Intelligent Computer Mathematics","author":"D M\u00fcller","year":"2017","unstructured":"M\u00fcller, D., Gauthier, T., Kaliszyk, C., Kohlhase, M., Rabe, F.: Classification of alignments between concepts of formal mathematical systems. In: Geuvers, H., England, M., Hasan, O., Rabe, F., Teschke, O. (eds.) CICM 2017. LNCS (LNAI), vol. 10383, pp. 83\u201398. Springer, Cham (2017). \n                    https:\/\/doi.org\/10.1007\/978-3-319-62075-6_7"},{"key":"5_CR8","first-page":"361","volume-title":"Logic and Computer Science","author":"LC Paulson","year":"1990","unstructured":"Paulson, L.C.: Isabelle: the next 700 theorem provers. In: Odifreddi, P. (ed.) Logic and Computer Science, pp. 361\u2013386. Academic Press, Cambridge (1990)"},{"key":"5_CR9","unstructured":"The QED Project (1996). \n                    http:\/\/www-unix.mcs.anl.gov\/qed\/"},{"key":"5_CR10","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/978-3-642-31374-5_10","volume-title":"Intelligent Computer Mathematics","author":"F Rabe","year":"2012","unstructured":"Rabe, F.: A query language for formal mathematical libraries. In: Jeuring, J., et al. (eds.) CICM 2012. LNCS (LNAI), vol. 7362, pp. 143\u2013158. Springer, Heidelberg (2012). \n                    https:\/\/doi.org\/10.1007\/978-3-642-31374-5_10\n                    \n                  . \n                    arXiv:1204.4685\n                    \n                   [cs.LO]"},{"key":"5_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.ic.2013.06.001","volume":"230","author":"Florian Rabe","year":"2013","unstructured":"Rabe, F., Kohlhase, M.: A scalable module system. Inf. Comput. 230, 1\u201354 (2013). \n                    http:\/\/kwarc.info\/frabe\/Research\/mmt.pdf","journal-title":"Information and Computation"},{"key":"5_CR12","unstructured":"ULO Documentation. \n                    https:\/\/ulo.mathhub.info\/\n                    \n                  . Accessed 03 Nov 2019"},{"key":"5_CR13","unstructured":"SPARQL 1.1 Overview. W3C Recommendation. World Wide Web Consortium (W3C), 23 March 2013. \n                    https:\/\/www.w3.org\/TR\/sparql11-overview\/"},{"key":"5_CR14","doi-asserted-by":"publisher","first-page":"71","DOI":"10.4204\/EPTCS.284.6","volume":"284","author":"Makarius Wenzel","year":"2018","unstructured":"Wenzel, M.: Isabelle\/jEdit as IDE for domain-specific formal languages and informal text documents. In: Masci, P., Monahan, R., Prevosto, V. (eds.) 4th Workshop on Formal Integrated Development Environment, F-IDE 2018 (2018). \n                    https:\/\/sketis.net\/wp-content\/uploads\/2018\/05\/isabelle-jedit-fide2018.pdf","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"5_CR15","unstructured":"Wenzel, M.: Isabelle\/MMT: export of Isabelle theories and import as OMDoc content. Blog entry (2018). \n                    https:\/\/sketis.net\/2018\/isabelle-mmt-export-of-isabelle-theories-and-import-as-omdoc-content"},{"key":"5_CR16","unstructured":"Wenzel, M.: Isabelle\/PIDE after 10 years of development. Presented at the UITP Workshop: User Interfaces for Theorem Provers (2018). \n                    https:\/\/sketis.net\/wp-content\/uploads\/2018\/08\/isabelle-pide-uitp2018.pdf"},{"key":"5_CR17","unstructured":"RDF Core Working Group of the W3C. Resource Description Framework Specification (2004). \n                    http:\/\/www.w3.org\/RDF\/"},{"key":"5_CR18","unstructured":"Coen, C.S.: A plugin to export Coq libraries to XML. In: 12th International Conference on Intelligent Computer Mathematics (CICM 19). LNAI (2019)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-23250-4_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,2]],"date-time":"2019-07-02T03:03:56Z","timestamp":1562036636000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-23250-4_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030232498","9783030232504"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-23250-4_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"3 July 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CICM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Intelligent Computer Mathematics","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 July 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mkm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cicm-conference.org\/2019\/cicm.php?event=&menu=general","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}