{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T13:57:49Z","timestamp":1725890269738},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540851097"},{"type":"electronic","value":"9783540851103"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-85110-3_34","type":"book-chapter","created":{"date-parts":[[2008,7,26]],"date-time":"2008-07-26T02:00:32Z","timestamp":1217037632000},"page":"398-414","source":"Crossref","is-referenced-by-count":2,"title":["Authoring Verified Documents by Interactive Proof Construction and Verification in Text-Editors"],"prefix":"10.1007","author":[{"given":"Dominik","family":"Dietrich","sequence":"first","affiliation":[]},{"given":"Ewaryst","family":"Schulz","sequence":"additional","affiliation":[]},{"given":"Marc","family":"Wagner","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"34_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/11618027_9","volume-title":"Mathematical Knowledge Management","author":"S. Autexier","year":"2006","unstructured":"Autexier, S., Benzm\u00fcller, C., Dietrich, D., Meier, A., Wirth, C.-P.: A generic modular data structure for proof attempts alternating on ideas and granularity. In: Kohlhase, M. (ed.) MKM 2005. LNCS (LNAI), vol.\u00a03863, pp. 126\u2013142. Springer, Heidelberg (2006)"},{"key":"34_CR2","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/11812289_9","volume-title":"Mathematical Knowledge Management","author":"S. Autexier","year":"2006","unstructured":"Autexier, S., Dietrich, D.: Synthesizing proof planning methods and oants agents from mathematical knowledge. In: Borwein, J.M., Farmer, W.M. (eds.) MKM 2006. LNCS (LNAI), vol.\u00a04108, pp. 94\u2013109. Springer, Heidelberg (2006)"},{"key":"34_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73086-6_16","volume-title":"Towards Mechanized Mathematical Assistants","author":"S. Autexier","year":"2007","unstructured":"Autexier, S., Fiedler, A., Neumann, T., Wagner, M.: Supporting user-defined notations when integrating scientific text-editors with proof assistance systems. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) MKM\/CALCULEMUS 2007. LNCS (LNAI), vol.\u00a04573, Springer, Heidelberg (2007)"},{"key":"34_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45719-4_34","volume-title":"Algebraic Methodology and Software Technology","author":"S. Autexier","year":"2002","unstructured":"Autexier, S., Hutter, D., Mossakowski, T., Schairer, A.: The development graph manager MAYA. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol.\u00a02422. Springer, Heidelberg (2002)"},{"key":"34_CR5","series-title":"LNCS (LNAI)","first-page":"67","volume-title":"MKM 2006","author":"S. Autexier","year":"2006","unstructured":"Autexier, S., Sacerdoti-Coen, C.: A formal correspondence between OMDoC with alternative proofs and the \n                      \n                        \n                      \n                      $\\bar{\\lambda}\\mu\\tilde{\\mu}$\n                    . In: Borwein, J.M., Farmer, W.M. (eds.) MKM 2006. LNCS (LNAI), vol.\u00a04108, pp. 67\u201381. Springer, Heidelberg (2006)"},{"key":"34_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/3-540-45306-7_16","volume-title":"Compiler Construction","author":"J. Aycock","year":"2001","unstructured":"Aycock, J., Horspool, N.: Directly-executable Earley parsing. In: Wilhelm, R. (ed.) CC 2001 and ETAPS 2001. LNCS, vol.\u00a02027, p. 229. Springer, Heidelberg (2001)"},{"key":"34_CR7","series-title":"LNCS (LNAI)","first-page":"367","volume-title":"LPAR 2002","author":"J. Siekmann","year":"2002","unstructured":"Siekmann, J., et al.: Proof development with \u03a9\n                    mega: \n                      \n                        \n                      \n                      $\\sqrt{2}$\n                     is irrational. In: Baaz, M., Voronkov, A. (eds.) LPAR 2002. LNCS (LNAI), vol.\u00a02514, pp. 367\u2013387. Springer, Heidelberg (2002)"},{"key":"34_CR8","volume-title":"Systems for Integrated Computation and Deduction","author":"A. Franke","year":"1999","unstructured":"Franke, A., Kohlhase, M.: MB\n                      \n                        \n                      \n                      ${\\sc ase}$\n                    : Representing mathematical knowledge in a relational data base. In: Systems for Integrated Computation and Deduction, Elsevier, Amsterdam (1999)"},{"key":"34_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73086-6_21","volume-title":"Towards Mechanized Mathematical Assistants","author":"K. Grue","year":"2007","unstructured":"Grue, K.: The Layers of Logiweb. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) MKM\/CALCULEMUS 2007. LNCS (LNAI), vol.\u00a04573, Springer, Heidelberg (2007)"},{"key":"34_CR10","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)"},{"key":"34_CR11","unstructured":"Lange, C.: A semantic wiki for mathematical knowledge management, Diploma thesis. IUB Bremen, Germany (2006)"},{"key":"34_CR12","unstructured":"Radzevich, S.: Semantic-based diff, patch and merge for XML-documents. Master thesis, Saarland University, Saarbr\u00fccken, Germany (April 2006)"},{"key":"34_CR13","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Towards Mechanized Mathematical Assistants","author":"C. Sacerdoti-Coen","year":"2007","unstructured":"Sacerdoti-Coen, C., Zacchiroli, S.: Spurious disambiguation error detection. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) MKM\/CALCULEMUS 2007. LNCS (LNAI), vol.\u00a04573, Springer, Heidelberg (2007)"},{"key":"34_CR14","volume-title":"Proceedings of the 9th Int","author":"A. Trybulec","year":"1985","unstructured":"Trybulec, A., Blair, H.: Computer assisted reasoning with Mizar. In: Joshi, A. (ed.) Proceedings of the 9th Int, Joint Conference on Artifical Intelligence. M. Kaufmann, San Francisco (1985)"},{"key":"34_CR15","unstructured":"J.v.d. Hoeven.: GNU \n                      \n                        \n                      \n                    \n                    MACS: A free, structured, WYSIWYG and technical text editor. Number 39-40 in Cahiers GUTenberg (May 2001)"},{"key":"34_CR16","volume-title":"7th Workshop on User Interfaces for Theorem Provers (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: Benzm\u00fcller, C., Autexier, S. (eds.) 7th Workshop on User Interfaces for Theorem Provers (UITP 2006). Elsevier, Amsterdam (2006)"},{"key":"34_CR17","unstructured":"Wenzel, M.: Isabelle\/Isar \u2014 a generic framework for human-readable proof documents. In: Matuszewski, R., Zalewska, A. (eds.) From Insight to Proof \u2014 Festschrift in Honour of Andrzej Trybulec. Studies in Logic, Grammar, and Rhetoric, University of Bialystok (2007)"}],"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-540-85110-3_34.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:14:50Z","timestamp":1619507690000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-85110-3_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540851097","9783540851103"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-85110-3_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}