{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:37Z","timestamp":1749124057216},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540590484"},{"type":"electronic","value":"9783540491781"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/bfb0014048","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T07:50:31Z","timestamp":1132732231000},"page":"109-123","source":"Crossref","is-referenced-by-count":22,"title":["Extracting text from proofs"],"prefix":"10.1007","author":[{"given":"Yann","family":"Coscoy","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gilles","family":"Kahn","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Laurent","family":"Th\u00e9ry","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"L. Magnusson, B. Nordstr\u00f6m, The ALF proof editor and Us proof engine, in Proceedings of the 1993 Types Worshop, Nijmegen, LNCS 806, 1994.","DOI":"10.1007\/3-540-58085-9_78"},{"key":"8_CR2","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":"8_CR3","unstructured":"A. Cohn, Proof Accounts in HOL, unpublished draft."},{"key":"8_CR4","unstructured":"Y. Coscoy, Traductions de preuves en langage naturel pour le systeme Coq, Rapport de Stage, Ecole Polytechnique, 1994."},{"key":"8_CR5","unstructured":"G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Paulin-Mohring, B. Werner, The Coq Proof Assistant User's Guide, INRIA Technical Report no. 134, 1991."},{"key":"8_CR6","unstructured":"Y. Bertot, the CtCoq Interface, available by ftp at babar.inria.fr: \/pub\/centaur\/ctcoq."},{"key":"8_CR7","unstructured":"N.G. de Bruijn, The Mathematical Vernacular, a language for Mathematics with typed sets in Proceedings from the Workshop on Programming Logic, P. Dybjer et al., Programming Methodology Group, Volume 37, University of G\u00f6teborg, 1987."},{"key":"8_CR8","unstructured":"A. Edgar, F.J. Pelletier, Natural language explanation of Natural Deduction proofs, in Proceedings of the First Conference of the Pacific Association for Computational Linguistics, Simon Fraser University, 1993."},{"key":"8_CR9","unstructured":"A. Felty, Proof explanation and revision, Technical Report, University of Pennsylvania MS-CIS-88-17, 1988."},{"key":"8_CR10","unstructured":"G. Gentzen, Investigations into logical deduction, in \u201cThe collected papers of Gerhard Gentzen\u201d, M.E. Szabo (Ed.), pp. 69\u2013131, North Holland, 1969."},{"key":"8_CR11","unstructured":"M.J.C. Gordon, T.F. Melham, HOL: a proof generating system for higher-order logic, Cambridge University Press, 1992."},{"key":"8_CR12","series-title":"LNAI 814","volume-title":"Proceedings of CADE-12","author":"X. Huang","year":"1994","unstructured":"X. Huang, Reconstructing Proofs at the Assertion Level, in Proceedings of CADE-12, Nancy, LNAI 814, Springer Verlag, 1994."},{"key":"8_CR13","unstructured":"Z. Luo, R. Pollack, LEGO proof development system: user's manual, Technical Report, University of Edinburgh, 1992."},{"key":"8_CR14","unstructured":"A. Massol, Presentation de Preuves en Langue Naturelle pour le Syst\u00e9me Coq, Rapport de DEA, Universite de Nice-Sophia-Antipolis, 1993."},{"key":"8_CR15","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"},{"key":"8_CR16","volume-title":"Une methode distribu\u00e9e de cr\u00e9ation d'interfaces et ses applications aux d\u00e9monstrateurs de theoremes, PhD","author":"L. Th\u00e9ry","year":"1994","unstructured":"L. Th\u00e9ry, Une methode distribu\u00e9e de cr\u00e9ation d'interfaces et ses applications aux d\u00e9monstrateurs de theoremes, PhD, Universite Denis Diderot, Paris, 1994."}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0014048","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T04:38:07Z","timestamp":1586579887000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0014048"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540590484","9783540491781"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/bfb0014048","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}