{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:31:23Z","timestamp":1725489083285},"publisher-location":"Berlin, Heidelberg","reference-count":19,"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_28","type":"book-chapter","created":{"date-parts":[[2007,8,14]],"date-time":"2007-08-14T10:57:56Z","timestamp":1187089076000},"page":"356-370","source":"Crossref","is-referenced-by-count":7,"title":["Extended Formula Normalization for \u03b5-Retrieval and Sharing of Mathematical Knowledge"],"prefix":"10.1007","author":[{"given":"Immanuel","family":"Normann","sequence":"first","affiliation":[]},{"given":"Michael","family":"Kohlhase","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"28_CR1","doi-asserted-by":"crossref","unstructured":"Bancerek, G.: On the structure of Mizar types. Electronic Notes in Theoretical Computer Science, 85(7) (2003)","DOI":"10.1016\/S1571-0661(04)80758-8"},{"key":"28_CR2","unstructured":"Bancerek, G., Kohlhase, M.: The mizar mathematical library in omdoc (submitted, 2007)"},{"key":"28_CR3","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"L. Robert","year":"1986","unstructured":"Robert, L., Constable, S., Allen, H., Bromly, W., Cleaveland, J., Cremer, R., Harper, D., Howe, T., Knoblock, N., Mendler, P., Panangaden, J., Sasaki, J., Smith, S.: Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs (1986)"},{"key":"28_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/3-540-61697-7_30","volume-title":"Design and Implementation of Symbolic Computation Systems","author":"S. Dalmas","year":"1996","unstructured":"Dalmas, S., Ga\u00ebtano, M., Huchet, C.: A deductive database for mathematical formulas. In: Limongelli, C., Calmet, J. (eds.) DISCO 1996. LNCS, vol.\u00a01128, pp. 287\u2013296. Springer, Heidelberg (1996)"},{"key":"28_CR5","unstructured":"H\u00e4hnle, R., Kerber, M., Weidenbach, C.: Common syntax of dfg-schwerpunktprogramm \u201cdeduktion\u201d. Interner Bericht 10\/96, Universit\u00e4t Karlsruhe, Fakult\u00e4t f\u00fcr Informatik (1996)"},{"key":"28_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/11856290_21","volume-title":"Artificial Intelligence and Symbolic Computation","author":"M. Kohlhase","year":"2006","unstructured":"Kohlhase, M., \u015eucan, I.: A search engine for mathematical formulae. In: Calmet, J., Ida, T., Wang, D. (eds.) AISC 2006. LNCS (LNAI), vol.\u00a04120, pp. 241\u2013253. Springer, Heidelberg (2006)"},{"key":"28_CR7","unstructured":"Kohlhase, M., \u015eucan, I.: System description: MathWebSearch 0.3, a semantic search engine. submitted to CADE 21 (2007)"},{"key":"28_CR8","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":"28_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/11618027_12","volume-title":"Mathematical Knowledge Management","author":"W. Naylor","year":"2006","unstructured":"Naylor, W., Padget, J.A.: Semantic matching for mathematical services. In: Kohlhase, M. (ed.) MKM 2005. LNCS (LNAI), vol.\u00a03863, pp. 174\u2013189. Springer, Heidelberg (2006)"},{"key":"28_CR10","unstructured":"The NuPrl online theory library. Internet interface at \n                    \n                      http:\/\/simon.cs.cornell.edu\/Info\/Projects\/NuPrl\/Nuprl4.2\/Libraries\/Welc.html"},{"key":"28_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction - CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) Automated Deduction - CADE-11. LNCS, vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"28_CR12","unstructured":"Pvs libraries, \n                    \n                      http:\/\/pvs.csl.sri.com\/libraries.html"},{"key":"28_CR13","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1006\/jsco.2001.0456","volume":"32","author":"P. Rudnicki","year":"2001","unstructured":"Rudnicki, P., Schwarzweller, C., Trybulec, A.: Commutative algebra in the Mizar system. Journal of Symbolic Computation\u00a032, 143\u2013169 (2001)","journal-title":"Journal of Symbolic Computation"},{"key":"28_CR14","unstructured":"Rudnicki, P.: An overview of the mizar project. In: Proceedings of the 1992 Workshop on Types and Proofs as Programs, pp. 311\u2013332 (1992)"},{"key":"28_CR15","unstructured":"Coq\u00a0Development Team. The Coq Proof Assistant Reference Manual. INRIA, see \n                    \n                      http:\/\/coq.inria.fr\/doc\/main.html"},{"issue":"1","key":"28_CR16","first-page":"9","volume":"1","author":"A. Trybulec","year":"1990","unstructured":"Trybulec, A.: Tarski Grothendieck set theory. Formalized Mathematics\u00a01(1), 9\u201311 (1990)","journal-title":"Formalized Mathematics"},{"key":"28_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/3-540-36469-2_16","volume-title":"Mathematical Knowledge Management","author":"J. Urban","year":"2003","unstructured":"Urban, J.: Translating mizar for first-order theorem provers. In: Asperti, A., Buchberger, B., Davenport, J.H. (eds.) MKM 2003. LNCS, vol.\u00a02594, pp. 203\u2013215. Springer, Heidelberg (2003)"},{"key":"28_CR18","series-title":"Lecture Notes in Computer Science","volume-title":"Automated Deduction - Cade-13","author":"C. Weidenbach","year":"1996","unstructured":"Weidenbach, C., Gaede, B., Rock, G.: Spass & flotter, version 0.42. In: McRobbie, M.A., Slaney, J.K. (eds.) Automated Deduction - Cade-13. LNCS, vol.\u00a01104, Springer, Heidelberg (1996)"},{"key":"28_CR19","unstructured":"Wiedijk, F.: Mizar: An impression (1999), \n                    \n                      http:\/\/www.cs.kun.nl\/~freek\/notes"}],"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_28.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T09:59:48Z","timestamp":1619517588000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73086-6_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540730835","9783540730866"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73086-6_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}