{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:31:08Z","timestamp":1725489068545},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540730835"},{"type":"electronic","value":"9783540730866"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73086-6_23","type":"book-chapter","created":{"date-parts":[[2007,8,14]],"date-time":"2007-08-14T06:57:56Z","timestamp":1187074676000},"page":"280-295","source":"Crossref","is-referenced-by-count":4,"title":["Restoring Natural Language as a Computerised Mathematics Input Method"],"prefix":"10.1007","author":[{"given":"Fairouz","family":"Kamareddine","sequence":"first","affiliation":[]},{"given":"Robert","family":"Lamar","sequence":"additional","affiliation":[]},{"given":"Manuel","family":"Maarek","sequence":"additional","affiliation":[]},{"given":"J. B.","family":"Wells","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"23_CR1","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":"23_CR2","unstructured":"LogiCal Project, INRIA Rocquencourt, France: The Coq Proof Assistant Reference Manual \u2013 Version 8.0 (2004), ftp:\/\/ftp.inria.fr\/INRIA\/coq\/V8.0\/doc\/"},{"key":"23_CR3","doi-asserted-by":"crossref","unstructured":"Audebaud, P., Rideau, L.: TeXmacs as authoring tool for publication and dissemination of formal developments. ENTCS, Rome, vol. 103, pp. 27\u201348 (2003)","DOI":"10.1016\/j.entcs.2004.09.012"},{"key":"23_CR4","unstructured":"Autexier, S., Benzm\u00fcller, C., Fiedler, A., Lesourd, H.: Integrating proof assistants as reasoning and verification tools into a scientific WYSIWIG (ed.) In: User Interfaces for Theorem Provers (UITP 2005) [Workshop], Edinburgh (2005)"},{"key":"23_CR5","unstructured":"Mamane, L.E., Geuvers, H.: A document-oriented Coq plugin for TeXmacs. In: Mathematical User-Interfaces Workshop 2006 [Workshop], Workingham (2006)"},{"key":"23_CR6","unstructured":"Rudnicki, P.: An overview of the Mizar project. In: Proceedings of the 1992 Workshop on Types for Proofs and Programs (1992)"},{"key":"23_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/3-540-48256-3_12","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Wenzel","year":"1999","unstructured":"Wenzel, M.: Isar \u2013 a generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 167\u2013184. Springer, Heidelberg (1999)"},{"key":"23_CR8","doi-asserted-by":"crossref","unstructured":"Autexier, S., Sacerdoti Coen, C.: A formal correspondence between OMDoc with alternative proofs and the $\\bar\\lambda\\mu\\tilde\\mu$ -calculus. [24],pp. 67\u201381","DOI":"10.1007\/11812289_7"},{"key":"23_CR9","doi-asserted-by":"crossref","unstructured":"Brown, C.E.: Verifying and invalidating textbook proofs using Scunak. [24], pp. 110\u2013123","DOI":"10.1007\/11812289_10"},{"key":"23_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":"23_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/3-540-44755-5_6","volume-title":"Theorem Proving in Higher Order Logics","author":"A. Asperti","year":"2001","unstructured":"Asperti, A., Padovani, L., Sacerdoti Coen, C., Schena, I.: HELM and the semantic math-web. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol.\u00a02152, pp. 59\u201374. Springer, Heidelberg (2001)"},{"key":"23_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"160","DOI":"10.1007\/978-3-540-27818-4_12","volume-title":"Mathematical Knowledge Management","author":"F. Kamareddine","year":"2004","unstructured":"Kamareddine, F., Maarek, M., Wells, J.B.: Flexible encoding of mathematics on the computer. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol.\u00a03119, pp. 160\u2013174. Springer, Heidelberg (2004)"},{"key":"23_CR13","doi-asserted-by":"crossref","unstructured":"Padovani, L., Zacchiroli, S.: From notation to semantics: There and back again. [24], pp. 194\u2013207","DOI":"10.1007\/11812289_16"},{"key":"23_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11618027_6","volume-title":"Mathematical Knowledge Management","author":"M. Kerber","year":"2006","unstructured":"Kerber, M., Pollet, M.: A tough nut for mathematical knowledge management. In: Kohlhase, M. (ed.) MKM 2005. LNCS (LNAI), vol.\u00a03863, pp. 81\u201395. Springer, Heidelberg (2006)"},{"key":"23_CR15","series-title":"Lecture Notes in Computer Science","first-page":"19","volume-title":"Mathematical Knowledge Management","author":"M. Pollet","year":"2004","unstructured":"Pollet, M., Sorge, V., Kerber, M.: Intuitive and formal representations: The case of matrices. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol.\u00a03119, pp. 19\u201321. Springer, Heidelberg (2004)"},{"key":"23_CR16","unstructured":"Gallian, J.A.: Contemporary Abstract Algebra. 5th edn. Houghton Mifflin Company (2002)"},{"key":"23_CR17","unstructured":"Kamareddine, F., Wells, J.: MathLang: A new language for mathematics, logic, and proof checking. A research proposal to UK funding body (2001)"},{"key":"23_CR18","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":"23_CR19","first-page":"8","volume":"38","author":"N.G. Bruijn de","year":"1991","unstructured":"de Bruijn, N.G.: Checking mathematics with computer assistance. Notices of the American Mathematical Society\u00a038, 8\u201315 (1991)","journal-title":"Notices of the American Mathematical Society"},{"key":"23_CR20","doi-asserted-by":"crossref","unstructured":"Kanahori, T., Sexton, A., Sorge, V., Suzuki, M.: Capturing abstract matrices from paper. [24], pp. 124\u2013138","DOI":"10.1007\/11812289_11"},{"key":"23_CR21","doi-asserted-by":"crossref","unstructured":"Raja, A., Rayner, M., Sexton, A., Sorge, V.: Towards a parser for mathematical formula recognition. [24], pp. 139\u2013151","DOI":"10.1007\/11812289_12"},{"key":"23_CR22","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1093\/comjnl\/27.2.97","volume":"27","author":"D.E. Knuth","year":"1984","unstructured":"Knuth, D.E.: Literate programming. The. Computer Journal\u00a027, 97\u2013111 (1984)","journal-title":"The Computer Journal"},{"key":"23_CR23","unstructured":"Farrell, P.: Grammatical Relations. Oxford Surveys in Syntax and Morphology. Oxford Linguistics (2005)"},{"key":"23_CR24","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Mathematical Knowledge Management","year":"2006","unstructured":"Borwein, J.M., Farmer, W.M. (eds.): MKM 2006. LNCS (LNAI), vol.\u00a04108. Springer, Heidelberg (2006)"}],"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_23.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T05:59:46Z","timestamp":1619503186000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73086-6_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540730835","9783540730866"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73086-6_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}