{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:27:46Z","timestamp":1761611266685},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540221647"},{"type":"electronic","value":"9783540248491"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24849-1_24","type":"book-chapter","created":{"date-parts":[[2010,8,8]],"date-time":"2010-08-08T16:34:24Z","timestamp":1281285264000},"page":"378-393","source":"Crossref","is-referenced-by-count":33,"title":["Formal Proof Sketches"],"prefix":"10.1007","author":[{"given":"Freek","family":"Wiedijk","sequence":"first","affiliation":[]}],"member":"297","reference":[{"unstructured":"Asperti, A., Wegner, B.: MOWGLI \u2013 A New Approach for the Content Description in Digital Documents. In: Proc. of the 9th Intl. Conference on Electronic Resources and the Social Role of Libraries in the Future, Autonomous Republic of Crimea, Ukraine, vol.\u00a01 (2002)","key":"24_CR1"},{"key":"24_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/3-540-36469-2_14","volume-title":"Mathematical Knowledge Management","author":"P. Cairns","year":"2003","unstructured":"Cairns, P., Gow, J.: A Theoretical Analysis of Hierarchical Proofs. In: Asperti, A., Buchberger, B., Davenport, J.H. (eds.) MKM 2003. LNCS, vol.\u00a02594, pp. 175\u2013187. Springer, Heidelberg (2003)"},{"key":"24_CR3","volume-title":"An Introduction to the Theory of Numbers","author":"G.H. Hardy","year":"1960","unstructured":"Hardy, G.H., Wright, E.M.: An Introduction to the Theory of Numbers, 4th edn. Clarendon Press, Oxford (1960)","edition":"4"},{"key":"24_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"313","DOI":"10.1007\/3-540-61511-3_97","volume-title":"Automated Deduction - Cade-13","author":"J. Harrison","year":"1996","unstructured":"Harrison, J.: Optimizing Proof Search in Model Elimination. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol.\u00a01104, pp. 313\u2013327. Springer, Heidelberg (1996)"},{"issue":"7","key":"24_CR5","doi-asserted-by":"publisher","first-page":"600","DOI":"10.2307\/2974556","volume":"102","author":"L. Lamport","year":"1995","unstructured":"Lamport, L.: How to Write a Proof. American Mathematical Monthly\u00a0102(7), 600\u2013608 (1995)","journal-title":"American Mathematical Monthly"},{"unstructured":"Muzalewski, M.: An Outline of PC Mizar. Fondation Philippe le Hodey, Brussels (1993), \n                  \n                    http:\/\/www.cs.kun.nl\/~freek\/mizar\/mizarmanual.ps.gz","key":"24_CR6"},{"unstructured":"Nederpelt, R.: Weak Type Theory, a formal language for mathematics. Technical Report 02-05, Eindhoven University of Technology, Department of Math. and Comp. Sc. (May 2002)","key":"24_CR7"},{"key":"24_CR8","doi-asserted-by":"crossref","first-page":"252","DOI":"10.1007\/3-540-58156-1_18","volume-title":"Proc. 12th Conference on Automated Deduction CADE","author":"G. Sutcliffe","year":"1994","unstructured":"Sutcliffe, G., Suttner, C., Yemenis, T.: The TPTP problem library. In: Bundy, A. (ed.) Proc. 12th Conference on Automated Deduction CADE, Nancy\/France, pp. 252\u2013266. Springer, Heidelberg (1994)"},{"key":"24_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/3-540-48256-3_14","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Syme","year":"1999","unstructured":"Syme, D.: Three Tactic Theorem Proving. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 203\u2013220. Springer, Heidelberg (1999)"},{"unstructured":"Th\u00e9ry, L.: Formal Proof Authoring: an Experiment. In: L\u00fcth, C., Aspinall, D. (eds.) UITP 2003, Rome, Technical Report No. 189, Institut f\u00fcr Informatik, Albert-Ludwigs Universit\u00e4t, Freiburg, September 2003, pp. 143\u2013159 (2003)","key":"24_CR10"},{"unstructured":"Wenzel, M.: Isabelle\/Isar \u2014 a versatile environment for human-readable formal proof documents. PhD thesis, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen (2002), \n                  \n                    http:\/\/tumb1.biblio.tu-muenchen.de\/publ\/diss\/in\/2002\/wenzel.html","key":"24_CR11"},{"unstructured":"Wiedijk, F.: Mizar: An Impression (1999), \n                  \n                    http:\/\/www.cs.kun.nl\/~freek\/mizar\/mizarintro.ps.gz","key":"24_CR12"},{"unstructured":"Wiedijk, F.: Formal proof sketches. In: Fokkink, W., van de Pol, J. (eds.) 7th Dutch Proof Tools Day, Program + Proceedings, Amsterdam (2003), CWI, \n                  \n                    http:\/\/www.cs.kun.nl\/~freek\/notes\/sketches.ps.gz","key":"24_CR13"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24849-1_24.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,2]],"date-time":"2021-05-02T23:15:15Z","timestamp":1619997315000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24849-1_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540221647","9783540248491"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24849-1_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}