{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:58:30Z","timestamp":1725551910128},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540314301"},{"type":"electronic","value":"9783540314318"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11618027_5","type":"book-chapter","created":{"date-parts":[[2006,1,19]],"date-time":"2006-01-19T06:48:07Z","timestamp":1137653287000},"page":"65-80","source":"Crossref","is-referenced-by-count":4,"title":["Assisted Proof Document Authoring"],"prefix":"10.1007","author":[{"given":"David","family":"Aspinall","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"L\u00fcth","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Burkhart","family":"Wolff","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/10930755_1","volume-title":"Theorem Proving in Higher Order Logics","author":"J.-R. Abrial","year":"2003","unstructured":"Abrial, J.-R., Cansell, D.: Click\u2019n\u2019prove: Interactive proofs within set theory. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 1\u201324. Springer, Heidelberg (2003)"},{"key":"5_CR2","unstructured":"Aspinall, D., L\u00fcth, C.: Commentary on PGIP (September 2003), Available from http:\/\/proofgeneral.inf.ed.ac.uk\/kit\/"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Aspinall, D., L\u00fcth, C.: Proof General meets IsaWin. In: Aspinall, D., L\u00fcth, C. (eds.) User Interfaces for Theorem Provers UITP 2003. ENTCS, vol.\u00a0103(C) (2003)","DOI":"10.1016\/j.entcs.2004.09.011"},{"key":"5_CR4","unstructured":"Aspinall, D., L\u00fcth, C.: Parsing, editing, proving: The PGIP display protocol. In: User Interfaces for Theorem Provers UITP 2005 (April 2005)"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Autexier, S., Benzm\u00fcller, C., Fiedler, A., Horacek, H., Bao Vo, Q.: Assertion level proof representation with underspecification. In: Kamareddine, F. (ed.) Proc. MKM Symposium MKM 2003, Edinburgh (November 2003)","DOI":"10.1016\/j.entcs.2003.12.026"},{"key":"5_CR6","unstructured":"Avigad, J.: Notes on a formalization of the prime number theorem. Technical report, Carnegie Mellon (2004)"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1007\/3-540-57887-0_94","volume-title":"Theoretical Aspects of Computer Software","author":"Y. Bertot","year":"1994","unstructured":"Bertot, Y., Kahn, G., Th\u00e9ry, L.: Proof by pointing. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol.\u00a0789, pp. 141\u2013160. Springer, Heidelberg (1994)"},{"issue":"2","key":"5_CR8","first-page":"152","volume":"9","author":"A.D. Brucker","year":"2003","unstructured":"Brucker, A.D., Rittinger, F., Wolff, B.: HOL-Z 2.0: A proof environment for Z-specifications. Journal of Universal Computer Science\u00a09(2), 152\u2013172 (2003)","journal-title":"Journal of Universal Computer Science"},{"key":"5_CR9","first-page":"589","volume-title":"Essays in Combinatory Logic, Lambda Calculus and Formalism","author":"N.G. Bruijn de","year":"1980","unstructured":"de Bruijn, N.G.: A survey of project Automath. In: Hindley, J.R., Curry, H.B. (eds.) Essays in Combinatory Logic, Lambda Calculus and Formalism, pp. 589\u2013606. Academic Press, London (1980)"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Dixon, L., Fleuriot, J.: A proof-centric approach to mathematical assistants. Journal of Applied Logic: Special Issue on Mathematics Assistance Systems (2005) (to appear)","DOI":"10.1016\/j.jal.2005.10.007"},{"key":"5_CR11","unstructured":"Gonthier, G.: A computer-checked proof of the four colour theorem. Technical report, Microsoft Research Cambridge (2004), http:\/\/research.microsoft.com\/~gonthier\/4colproof.pdf"},{"key":"5_CR12","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1093\/comjnl\/39.4.291","volume":"39","author":"J. Grundy","year":"1996","unstructured":"Grundy, J.: Transformational hierarchical reasoning. Computer Journal\u00a039, 291\u2013302 (1996)","journal-title":"Computer Journal"},{"key":"5_CR13","unstructured":"Hales, T.C.: The Flyspeck project page., http:\/\/www.math.pitt.edu\/~thales\/flyspeck\/index.html"},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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)"},{"issue":"3","key":"5_CR15","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1023\/B:JLLI.0000028393.47593.b8","volume":"13","author":"F. Kamareddine","year":"2004","unstructured":"Kamareddine, F., Nederpelt, R.: A refinement of deBruijn\u2019s formal language of mathematics. Journal of Logic, Language and Information\u00a013(3), 287\u2013340 (2004)","journal-title":"Journal of Logic, Language and Information"},{"issue":"2","key":"5_CR16","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(2), 97\u2013111 (1984)","journal-title":"The Computer Journal"},{"key":"5_CR17","unstructured":"Kohlhase, M.: Semantic markup for TeX\/LaTeX. In: Informal Proc. Mathematical User Interfaces, Math UI 2004 (2004)"},{"issue":"2","key":"5_CR18","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1017\/S0956796899003421","volume":"9","author":"C. L\u00fcth","year":"1999","unstructured":"L\u00fcth, C., Wolff, B.: Functional design and implementation of graphical user interfaces for theorem provers. Journal of Functional Programming\u00a09(2), 167\u2013189 (1999)","journal-title":"Journal of Functional Programming"},{"key":"5_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/3-540-44659-1_25","volume-title":"Theorem Proving in Higher Order Logics","author":"C. L\u00fcth","year":"2000","unstructured":"L\u00fcth, C., Wolff, B.: TAS \u2014 a generic window inference system. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol.\u00a01869, pp. 405\u2013422. Springer, Heidelberg (2000)"},{"key":"5_CR20","first-page":"1402","volume":"307","author":"D. Mackenzie","year":"2005","unstructured":"Mackenzie, D.: What in the name of Euclid is going on here? Science\u00a0307, 1402\u20131403 (2005)","journal-title":"Science"},{"key":"5_CR21","unstructured":"Relax Ng Xml schema language (2003), Home page at http:\/\/www.relaxng.org\/"},{"key":"5_CR22","unstructured":"Th\u00e9ry, L.: Formal proof authoring: An experiment. In: Informal Proc. User Interfaces for Theorem Provers, UITP 2003 (2003)"},{"key":"5_CR23","unstructured":"Trybulec, A., et al.: The Mizar project. University of Bialystok, Poland (1973), See web page hosted at http:\/\/mizar.org"},{"key":"5_CR24","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 \u2014 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, p. 167. Springer, Heidelberg (1999)"},{"key":"5_CR25","unstructured":"Wenzel, M.: Isabelle\/Isar \u2014 a versatile environment for human-readable formal proof documents. PhD thesis, Technische Universit\u00e4t M\u00fcnchen (2001)"},{"key":"5_CR26","doi-asserted-by":"crossref","unstructured":"Winterstein, D., Aspinall, D., L\u00fcth, C.: Proof General\/Eclipse. In: User Interfaces for Theorem Provers UITP 2005 (2005)","DOI":"10.1145\/1188835.1188845"}],"container-title":["Lecture Notes in Computer Science","Mathematical Knowledge Management"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11618027_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,6]],"date-time":"2023-05-06T02:42:58Z","timestamp":1683340978000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11618027_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540314301","9783540314318"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/11618027_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}