{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:31:27Z","timestamp":1725489087784},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540730835"},{"type":"electronic","value":"9783540730866"}],"license":[{"start":{"date-parts":[[2007,1,1]],"date-time":"2007-01-01T00:00:00Z","timestamp":1167609600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-73086-6_16","type":"book-chapter","created":{"date-parts":[[2007,8,14]],"date-time":"2007-08-14T06:57:56Z","timestamp":1187074676000},"page":"176-190","source":"Crossref","is-referenced-by-count":2,"title":["Supporting User-Defined Notations When Integrating Scientific Text-Editors with Proof Assistance Systems"],"prefix":"10.1007","author":[{"given":"Serge","family":"Autexier","sequence":"first","affiliation":[]},{"given":"Armin","family":"Fiedler","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Neumann","sequence":"additional","affiliation":[]},{"given":"Marc","family":"Wagner","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"16_CR1","unstructured":"Mathematical Markup Language (MathML)\u00a0Version 2.0. W3c recommendation 21 february 2001. Technical report (2003), \n                    \n                      http:\/\/www.w3.org\/TR\/MathML2"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Asperti, A., Sacerdoti-Coen, C., Tassi, E., Zacchiroli, S.: User interaction with the matita proof assistant. Journal of Automated Reasoning, Special Issue on User Interfaces for Theorem Proving (2007)","DOI":"10.1007\/s10817-007-9070-5"},{"key":"16_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1007\/978-3-540-27818-4_25","volume-title":"Mathematical Knowledge Management","author":"C.S. Coen","year":"2004","unstructured":"Coen, C.S., Zacchiroli, S.: Efficient ambiguous parsing of mathematical formulae. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol.\u00a03119, pp. 347\u2013362. Springer, Heidelberg (2004)"},{"key":"16_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/11618027_15","volume-title":"Mathematical Knowledge Management","author":"F. Kamareddine","year":"2006","unstructured":"Kamareddine, F., Maarek, M., Wells, J.B.: Toward an object-oriented structure for mathematical text. In: Kohlhase, M. (ed.) MKM 2005. LNCS (LNAI), vol.\u00a03863, pp. 217\u2013233. Springer, Heidelberg (2006)"},{"key":"16_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","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)"},{"issue":"1-2","key":"16_CR6","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1016\/j.jlap.2005.09.005","volume":"67","author":"T. Mossakowski","year":"2006","unstructured":"Mossakowski, T., Autexier, S., Hutter, D.: Development graphs - proof management for structured specifications. Journal of Logic and Algebraic Programming, special issue on Algebraic Specification and Development Techniques\u00a067(1-2), 114\u2013145 (2006)","journal-title":"Journal of Logic and Algebraic Programming, special issue on Algebraic Specification and Development Techniques"},{"key":"16_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"16_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/11812289_16","volume-title":"Mathematical Knowledge Management","author":"L. Padovani","year":"2006","unstructured":"Padovani, L., Zacchiroli, S.: From notation to semantics: There and back again! In: Borwein, J.M., Farmer, W.M. (eds.) MKM 2006. LNCS (LNAI), vol.\u00a04108, Springer, Heidelberg (2006)"},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"Bundy, A., McCasland, R.: Mathsaid: A mathematical theorem discovery tool. In: Proceedings of SYNASC 2006 (2006)","DOI":"10.1109\/SYNASC.2006.51"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"van\u00a0der Hoeven, J.: Gnu TEXMACS: A free, structured, wysiwyg and technical text editor. Number 39-40 in Cahiers GUTenberg (May 2001)","DOI":"10.5802\/cg.292"},{"key":"16_CR11","unstructured":"Wagner, M.: Mediation between text-editors and proof assistance systems. Diploma thesis, Saarland University, Saarbr\u00fccken, Germany (2006)"},{"key":"16_CR12","series-title":"ENTCS","volume-title":"UITP 2006","author":"M. Wagner","year":"2006","unstructured":"Wagner, M., Autexier, S., Benzm\u00fcller, C.: Plat\u03a9: A mediator between text-editors and proof assistance systems. In: Autexier, S., Benzm\u00fcller, C. (eds.) UITP 2006. 7th Workshop on User Interfaces for Theorem Provers. ENTCS, Elsevier, North-Holland (2006)"},{"key":"16_CR13","volume-title":"Compiler Construction","author":"W. Waite","year":"1985","unstructured":"Waite, W., Goos, G.: Compiler Construction. Springer, Heidelberg (1985)"},{"key":"16_CR14","volume-title":"\u00dcbersetzerbau - Theorie, Konstruktion, Generierung, 2. Auflage","author":"R. Wilhelm","year":"1997","unstructured":"Wilhelm, R., Maurer, D.: \u00dcbersetzerbau - Theorie, Konstruktion, Generierung, 2. Auflage. Springer, Heidelberg (1997)"}],"container-title":["Lecture Notes in Computer Science","Towards Mechanized Mathematical Assistants"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73086-6_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T20:58:49Z","timestamp":1558472329000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73086-6_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540730835","9783540730866"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73086-6_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}