{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T16:05:55Z","timestamp":1725465955317},"publisher-location":"Berlin, Heidelberg","reference-count":6,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540637004"},{"type":"electronic","value":"9783540696315"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/bfb0052156","type":"book-chapter","created":{"date-parts":[[2006,6,7]],"date-time":"2006-06-07T00:43:12Z","timestamp":1149640992000},"page":"149-167","source":"Crossref","is-referenced-by-count":4,"title":["A natural language explanation for formal proofs"],"prefix":"10.1007","author":[{"given":"Yann","family":"Coscoy","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,5,16]]},"reference":[{"key":"9_CR1","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1016\/0004-3702(76)90007-2","volume":"7","author":"D. Chester","year":"1976","unstructured":"D. Chester, The translation of Formal Proofs into English, Artificial Intelligence 7 (1976), 261\u2013278, 1976.","journal-title":"Artificial Intelligence"},{"key":"9_CR2","unstructured":"C. Cornes, J. Courant, J-C. Filli\u00e2tre, E. Gimenez, G. Huet, P. Manoury, C. Mu\u00f1oz, C. Murthy, C. Parent, C. Paulin-Mohring, A. Sa\u00cfbi, B. Werner, The Coq Proof Assistant Reference Manual, INRIA."},{"key":"9_CR3","unstructured":"Y. Coscoy, G. Kahn, L. Th\u00e9ry, Extracting Text from Proofs, in Typed Lambda Calculus and Applications, volume 902 of Lecture Notes in Computer Science. Springer-Verlag."},{"key":"9_CR4","unstructured":"X. Huang, Human Oriented Proof Presentation: A Reconstructive Approach, SEKI Report SR-SR-94-07, UNIVERSIT\u00e4T DES SAARLANDES,."},{"key":"9_CR5","unstructured":"K. Prazmowski, P.Rudnicki Mizar-MSE Primer Warsaw University, University of Alberta."},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"A. Ranta, Type Theory and the Informal Language of Mathematics, in Proceedings of the 1993 Types Worshop, Nijmegen, LNCS 806, 1994.","DOI":"10.1007\/3-540-58085-9_84"}],"container-title":["Lecture Notes in Computer Science","Logical Aspects of Computational Linguistics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0052156","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,19]],"date-time":"2019-04-19T02:25:33Z","timestamp":1555640733000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0052156"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540637004","9783540696315"],"references-count":6,"URL":"https:\/\/doi.org\/10.1007\/bfb0052156","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}