{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T05:53:59Z","timestamp":1725515639078},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642313738"},{"type":"electronic","value":"9783642313745"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31374-5_12","type":"book-chapter","created":{"date-parts":[[2012,6,25]],"date-time":"2012-06-25T13:00:57Z","timestamp":1340629257000},"page":"169-185","source":"Crossref","is-referenced-by-count":4,"title":["Point-and-Write \u2013 Documenting Formal Mathematics by Reference"],"prefix":"10.1007","author":[{"given":"Carst","family":"Tankink","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Lange","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Josef","family":"Urban","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"12_CR1","unstructured":"Resource Description Framework (RDF): Concepts and abstract syntax. Recommendation, W3C (2004), http:\/\/www.w3.org\/TR\/rdf-concepts"},{"key":"12_CR2","unstructured":"RDFa in XHTML: Syntax and processing. Recommendation, W3C (October 2008), http:\/\/www.w3.org\/TR\/rdfa-syntax"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Asperti, A., Geuvers, H., Loeb, I., Mamane, L.E., Coen, C.S.: An interactive algebra course with formalised proofs and definitions. In: Kohlhase [14], pp. 315\u2013329","DOI":"10.1007\/11618027_21"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","volume-title":"Intelligent Computer Mathematics","year":"2010","unstructured":"Autexier, S., Calmet, J., Delahaye, D., Ion, P.D.F., Rideau, L., Rioboo, R., Sexton, A.P. (eds.): AISC 2010. LNCS, vol.\u00a06167. Springer, Heidelberg (2010)"},{"key":"12_CR5","unstructured":"Bancerek, G., Kohlhase, M.: Towards a Mizar Mathematical Library in OMDoc format. In: Matuszewski, R., Zalewska, A. (eds.) From Insight to Proof: Festschrift in Honour of Andrzej Trybulec. Studies in Logic, Grammar and Rhetoric, vol.\u00a010(23), pp. 265\u2013275. University of Bia\u0142ystok (2007)"},{"issue":"3-4","key":"12_CR6","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1023\/A:1021966832558","volume":"29","author":"G. Bancerek","year":"2002","unstructured":"Bancerek, G., Rudnicki, P.: A compendium of continuous lattices in MIZAR. J. Autom. Reasoning\u00a029(3-4), 189\u2013224 (2002)","journal-title":"J. Autom. Reasoning"},{"key":"12_CR7","unstructured":"Blackwell, A.F., Green, T.R.G.: Cognitive dimensions of information artefacts: a tutorial. Tutorial (1998), http:\/\/www.cl.cam.ac.uk\/~afb21\/CognitiveDimensions\/CDtutorial.pdf"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Cairns, P., Gow, J.: Literate proving: Presenting and documenting formal proofs. In: Kohlhase (ed.) [14], pp. 159\u2013173","DOI":"10.1007\/11618027_11"},{"key":"12_CR9","unstructured":"The Coq wiki, Browsable online at http:\/\/coq.inria.fr\/cocorico"},{"key":"12_CR10","unstructured":"The Coq mailing list, coq-club@inria.fr"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Heath, T., Bizer, C.: Linked Data: Evolving the Web into a Global Data Space. Morgan & Claypool (2011)","DOI":"10.1007\/978-3-642-24577-0_1"},{"key":"12_CR12","unstructured":"Heinz, C., Moses, B.: The listings package. Technical report, CTAN (2007), http:\/\/www.ctan.org\/tex-archive\/macros\/latex\/contrib\/listings"},{"key":"12_CR13","unstructured":"The Isabelle mailing list, cl-isabelle-users@lists.cam.ac.uk"},{"key":"12_CR14","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Mathematical Knowledge Management","year":"2006","unstructured":"Kohlhase, M. (ed.): MKM 2005. LNCS (LNAI), vol.\u00a03863. Springer, Heidelberg (2006)"},{"key":"12_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/11826095","volume-title":"OMDoc \u2013 An Open Markup Format for Mathematical Documents [version 1.2]","author":"M. Kohlhase","year":"2006","unstructured":"Kohlhase, M.: OMDoc \u2013 An Open Markup Format for Mathematical Documents [version 1.2]. LNCS (LNAI), vol.\u00a04180. Springer, Heidelberg (2006)"},{"key":"12_CR16","unstructured":"Lange, C.: OMDoc ontology (2011), http:\/\/kwarc.info\/projects\/docOnto\/omdoc.html"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Lange, C.: Ontologies and languages for representing mathematical knowledge on the semantic web. Semantic Web Journal (in press, 2012)","DOI":"10.3233\/SW-2012-0059"},{"key":"12_CR18","unstructured":"Lange, C., Urban, J. (eds.): Proceedings of the ITP 2011 Workshop on Mathematical Wikis (MathWikis). CEUR-WS, vol.\u00a0767 (2011)"},{"key":"12_CR19","unstructured":"The Mizar mailing list, mizar-forum@mizar.uwb.edu.pl"},{"key":"12_CR20","unstructured":"The Mizar wiki, Browsable online at http:\/\/wiki.mizar.org"},{"key":"12_CR21","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1145\/1296951.1296966","volume-title":"WikiSym 2007","author":"C. Sauer","year":"2007","unstructured":"Sauer, C., Smith, C., Benz, T.: Wikicreole: a common wiki markup. In: WikiSym 2007, pp. 131\u2013142. ACM, New York (2007)"},{"key":"12_CR22","unstructured":"The homotopy type theory blog, http:\/\/homotopytypetheory.org\/"},{"key":"12_CR23","doi-asserted-by":"crossref","unstructured":"Urban, J.: XML-izing Mizar: making semantic processing and presentation of MML easy. In: Kohlhase (ed.) [14], pp. 346\u2013360","DOI":"10.1007\/11618027_23"},{"key":"12_CR24","doi-asserted-by":"crossref","unstructured":"Urban, J., Alama, J., Rudnicki, P., Geuvers, H.: A wiki for Mizar: Motivation, considerations, and initial prototype. In: Autexier, et al. (eds.) [4], pp. 455\u2013469","DOI":"10.1007\/978-3-642-14128-7_38"},{"key":"12_CR25","doi-asserted-by":"crossref","unstructured":"Urban, J., Sutcliffe, G.: Automated reasoning and presentation support for formalizing mathematics in Mizar. In: Autexier, et al. (eds.) [4], pp. 132\u2013146","DOI":"10.1007\/978-3-642-14128-7_12"},{"key":"12_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22863-6","volume-title":"Interactive Theorem Proving","author":"M.C.J.D. Eekelen van","year":"2011","unstructured":"van Eekelen, M.C.J.D., Geuvers, H., Schmaltz, J., Wiedijk, F.: ITP 2011. LNCS, vol.\u00a06898. Springer, Heidelberg (2011)"},{"key":"12_CR27","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-642-22673-1_17","volume-title":"Intelligent Computer Mathematics","author":"M. Wenzel","year":"2011","unstructured":"Wenzel, M.: Isabelle as Document-Oriented Proof Assistant. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) Calculemus\/MKM 2011. LNCS (LNAI), vol.\u00a06824, pp. 244\u2013259. Springer, Heidelberg (2011)"},{"key":"12_CR28","unstructured":"Wenzel, M.M.: Isabelle\/Isar \u2014 a versatile environment for human-readable formal proof documents. PhD thesis, Technische Universit\u00e4t M\u00fcnchen (2002)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31374-5_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,9]],"date-time":"2020-07-09T21:49:41Z","timestamp":1594331381000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31374-5_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642313738","9783642313745"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31374-5_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}