{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:48:50Z","timestamp":1725490130114},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540420712"},{"type":"electronic","value":"9783540449904"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44990-6_4","type":"book-chapter","created":{"date-parts":[[2007,8,28]],"date-time":"2007-08-28T14:20:43Z","timestamp":1188310843000},"page":"53-64","source":"Crossref","is-referenced-by-count":0,"title":["On Communicating Proofs in Interactive Mathematical Documents"],"prefix":"10.1007","author":[{"given":"Olga","family":"Caprotti","sequence":"first","affiliation":[]},{"given":"Martijn","family":"Oostdijk","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,5,11]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"P. Bertoli, J. Calmet, F. Giunchiglia, and K. Homann. Specification and Integration of Theorem Provers and Computer Algebra Systems. In J. Calmet and J. Plaza, editors, Artificial Intelligence and Symbolic Computation: International Conference AISC'98, volume 1476 of Lecture Notes in Artificial Intelligence, Plattsburgh, New York, USA, September 1998.","DOI":"10.1007\/BFb0055905"},{"key":"4_CR2","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1006\/jsco.1997.0171","volume":"25","author":"Y. Bertot","year":"1998","unstructured":"Yves Bertot and Laurent Th\u00e9ry. A Generic Approach to Building User Interfaces for Theorem Provers. Journal of Symbolic Computation, 25:161\u2013194, 1998.","journal-title":"Journal of Symbolic Computation"},{"key":"4_CR3","unstructured":"Stephen Buswell, Stan Devitt, Angel Diaz, Bruce Smith, Neil Soiffer, Robert Sutor, Stephen Watt, St\u00e9phane Dalmas, David Carlisle, Roger Hunter, and Ron Ausbrooks. Mathematical Markup Language (MathML) Version 2.0. W3C Working Draft 11 February 2000, February 2000. Available at http:\/\/www.w3.org\/TR\/2000\/WD-MathML2-20000211\/ ."},{"key":"4_CR4","unstructured":"O. Caprotti and M. Oostdijk. How to formally and efficiently prove prime(2999). In Proceedings of Calculemus 2000, St. Andrews, 2000."},{"key":"4_CR5","unstructured":"[5] O. Caprotti and M. N. Riem. Server-side Presentation of OpenMath Documents using MathML. Submitted."},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Olga Caprotti and Arjeh Cohen. Connecting proof checkers and computer algebra using OpenMath. In The 12th International Conference on Theorem Proving in Higher Order Logics, Nice, France, September 1999.","DOI":"10.1007\/3-540-48256-3_8"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Olga Caprotti and Arjeh Cohen. Integrating Computational and Deduction Systems Using OpenMath. In Proceedings of Calculemus 99, Trento, July 1999.","DOI":"10.1016\/S1571-0661(05)80616-4"},{"key":"4_CR8","unstructured":"A. M. Cohen, H. Cuypers, and H. Sterk. Algebra Interactive, interactive course material. Number ISBN 3-540-65368-6. SV, 1999."},{"key":"4_CR9","unstructured":"R. L. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R.W. Harper, D. J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, J. T. Sasaki, and S. F. Smith. Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, 1986. URL http:\/\/simon.cs.cornell.edu\/Info\/Projects\/NuPrl\/nuprl.html ."},{"key":"4_CR10","series-title":"Lect Notes Comput Sci","volume-title":"A natural language explanation for formal proofs","author":"Y. Coscoy","year":"1997","unstructured":"Y. Coscoy. A natural language explanation for formal proofs. In C. Retor\u00e9, editor, Proceedings of Int. Conf. on Logical Aspects of Computational Liguistics (LACL), Nancy, volume 1328. Springer-Verlag LNCS\/LNAI, September 1996."},{"key":"4_CR11","series-title":"Lect Notes Comput Sci","volume-title":"Extracting text from proof","author":"Y. Coscoy","year":"1995","unstructured":"Y. Coscoy, G. Kahn, and L. Th\u00e9ry. Extracting text from proof. In M. Dezani and G. Plotkin, editors, Proceedings of Int. Conf. on Typed Lambda-Calculus and Applications (TLCA), Edinburgh, volume 902. Springer-Verlag LNCS, April 1995."},{"issue":"3","key":"4_CR12","first-page":"156","volume":"5","author":"A. Franke","year":"1999","unstructured":"A. Franke, S. Hess, Ch. Jung, M. Kohlhase, and V. Sorge. Agent-Oriented Integration of Distributed Mathematical Services. Journal of Universal Computer Science, 5(3):156\u2013187, March 1999. Special issue on Integration of Deduction System.","journal-title":"Journal of Universal Computer Science"},{"key":"4_CR13","unstructured":"Amanda M. Holland-Minkley, Regina Barzilay, and Robert Constable. Verbalization of high-level formal proofs. In Sixteenth National Conference on Artificial Intelligence, 1999."},{"key":"4_CR14","unstructured":"M. Kohlhase. MBASE: Representing mathematical knowledge in a relational data base. In Calculemus '99 Workshop, Trento, Italy, July 1999."},{"key":"4_CR15","unstructured":"M. Kohlhase. OMDOC: Towards an Openmath Representation of Mathematical Documents. Technical report, DFKI, Saarbr\u00fccken, 1999."},{"key":"4_CR16","unstructured":"Pascal Lequang, Yves Bertot, Laurence Rideau, and Lo\u00cfc Pottier. Pcoq: A graphical user-interface for Coq. http:\/\/www-sop.inria.fr\/lemme\/pcoq\/ , February 2000."},{"key":"4_CR17","series-title":"Lect Notes Comput Sci","volume-title":"Mathematical Vernacular and Conceptual Wellformedness in Mathematical Language","author":"Z. Luo","year":"1997","unstructured":"Z. Luo and P. Callaghan. Mathematical Vernacular and Conceptual Wellformedness in Mathematical Language. In Proceedings of the 2nd International Conference on Logical Aspects of Computational Linguistics 97, volume 1582 of Lecture Notes in Computer Science, Nancy, 1997."},{"key":"4_CR18","unstructured":"Z. Luo and R. Pollack. LEGO Proof Development System: User\u2019s Manual. Department of Compter Science, University of Edinburgh, 1992."},{"key":"4_CR19","unstructured":"R. P. Nederpelt, J. H. Geuvers, and R. C. de Vrijer, editors. Selected Papers on Automath, volume 133 of Studies in logic and the Foundations of Mathematics. Elsevier, 1994."},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"Paulo Ribenboim. The New Book of Prime Number Records. Number ISBN 0-387-94457-5. SV, 1996.","DOI":"10.1007\/978-1-4612-0759-7"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"Jurgen Richter-Gebert and Ulrich H. Kortenkamp. The Interactive Geometry Software Cinderella (Interactive Geometry on Computers). Number ISBN 3540147195. SV, July 1999.","DOI":"10.1007\/978-3-642-58318-6"},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"Paul Wang. Design and Protocol for Internet Accessible Mathematical Computation. Technical Report ICM-199901-001, ICM\/Kent State University, January 1999.","DOI":"10.1145\/309831.309961"}],"container-title":["Lecture Notes in Computer Science","Artificial Intelligence and Symbolic Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44990-6_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,2]],"date-time":"2019-05-02T17:08:06Z","timestamp":1556816886000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44990-6_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540420712","9783540449904"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-44990-6_4","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}