{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T05:54:00Z","timestamp":1725515640723},"publisher-location":"Berlin, Heidelberg","reference-count":10,"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_28","type":"book-chapter","created":{"date-parts":[[2012,6,25]],"date-time":"2012-06-25T13:00:57Z","timestamp":1340629257000},"page":"417-421","source":"Crossref","is-referenced-by-count":5,"title":["A Web Interface for Matita"],"prefix":"10.1007","author":[{"given":"Andrea","family":"Asperti","sequence":"first","affiliation":[]},{"given":"Wilmer","family":"Ricciotti","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"28_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/978-3-642-22673-1_10","volume-title":"Intelligent Computer Mathematics","author":"J. Alama","year":"2011","unstructured":"Alama, J., Brink, K., Mamane, L., Urban, J.: Large Formal Wikis: Issues and Solutions. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) MKM 2011 and Calculemus 2011. LNCS, vol.\u00a06824, pp. 133\u2013148. Springer, Heidelberg (2011)"},{"key":"28_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-642-22438-6_7","volume-title":"Automated Deduction \u2013 CADE-23","author":"A. Asperti","year":"2011","unstructured":"Asperti, A., Ricciotti, W., Sacerdoti Coen, C., Tassi, E.: The Matita Interactive Theorem Prover. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol.\u00a06803, pp. 64\u201369. Springer, Heidelberg (2011)"},{"issue":"2","key":"28_CR3","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/s10817-007-9070-5","volume":"39","author":"A. Asperti","year":"2007","unstructured":"Asperti, A., Sacerdoti Coen, C., Tassi, E., Zacchiroli, S.: User interaction with the Matita proof assistant. Journal of Automated Reasoning\u00a039(2), 109\u2013139 (2007)","journal-title":"Journal of Automated Reasoning"},{"key":"28_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/3-540-46419-0_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Aspinall","year":"2000","unstructured":"Aspinall, D.: Proof General: A Generic Tool for Proof Development. In: Graf, S. (ed.) TACAS 2000. LNCS, vol.\u00a01785, pp. 38\u201343. Springer, Heidelberg (2000)"},{"key":"28_CR5","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1006\/jsco.1997.0171","volume":"25","author":"Y. Bertot","year":"1998","unstructured":"Bertot, Y., Th\u00e9ry, L.: A generic approach to building user interfaces for theorem provers. Journal of Symbolic Computation\u00a025, 161\u2013194 (1998)","journal-title":"Journal of Symbolic Computation"},{"issue":"1","key":"28_CR6","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s12046-009-0001-5","volume":"34","author":"H. Geuvers","year":"2009","unstructured":"Geuvers, H.: Proof Assistants: history, ideas and future. Sadhana\u00a034(1), 3\u201325 (2009)","journal-title":"Sadhana"},{"issue":"2","key":"28_CR7","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/j.entcs.2006.09.021","volume":"174","author":"C. Kaliszyk","year":"2007","unstructured":"Kaliszyk, C.: Web interfaces for proof assistants. Electr. Notes Theor. Comput. Sci.\u00a0174(2), 49\u201361 (2007)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"28_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/978-3-642-14128-7_37","volume-title":"Intelligent Computer Mathematics","author":"C. Tankink","year":"2010","unstructured":"Tankink, C., Geuvers, H., McKinna, J., Wiedijk, F.: Proviola: A Tool for Proof Re-animation. In: Autexier, S., Calmet, J., Delahaye, D., Ion, P.D.F., Rideau, L., Rioboo, R., Sexton, A.P. (eds.) AISC 2010. LNCS, vol.\u00a06167, pp. 440\u2013454. Springer, Heidelberg (2010)"},{"key":"28_CR9","doi-asserted-by":"crossref","unstructured":"Urban, J., Alama, J., Rudnicki, P., Geuvers, H.: A wiki for mizar: Motivation, considerations, and initial prototype. CoRR, abs\/1005.4552 (2010)","DOI":"10.1007\/978-3-642-14128-7_38"},{"key":"28_CR10","series-title":"Lecture Notes in Computer Science","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.) MKM 2011 and Calculemus 2011. LNCS, vol.\u00a06824, pp. 244\u2013259. Springer, Heidelberg (2011)"}],"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_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T13:17:08Z","timestamp":1556889428000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31374-5_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642313738","9783642313745"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31374-5_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}