{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T06:24:56Z","timestamp":1725690296197},"publisher-location":"Wiesbaden","reference-count":28,"publisher":"Vieweg+Teubner Verlag","isbn-type":[{"type":"print","value":"9783519026464"},{"type":"electronic","value":"9783322912305"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/978-3-322-91230-5_9","type":"book-chapter","created":{"date-parts":[[2012,7,4]],"date-time":"2012-07-04T21:46:58Z","timestamp":1341438418000},"page":"150-165","source":"Crossref","is-referenced-by-count":0,"title":["Darstellung formaler Beweise"],"prefix":"10.1007","author":[{"given":"Martin","family":"Simons","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"9_CR1","unstructured":"Anlauff, M. (1995), Rechnerunterst\u00fctzung formaler Beweissprachen,GMD-Bericht Nr. 244, R. Oldenbourg Verlag."},{"key":"9_CR2","unstructured":"Backhouse, R. C. (1989), \u2018Making formality work for us\u2019, Bulletin of the EATCS (38), 219\u2013249."},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Backhouse, R. C. (1995), \u2018The calculational method\u2019, Information Processing Letters 53. Special issue on the calculational method.","DOI":"10.1016\/0020-0190(94)00212-H"},{"key":"9_CR4","volume-title":"TU Berlin","author":"M Biersack","year":"1993","unstructured":"Biersack, M., Raschke, R. & Simons, M. (1993), The DevaWEB system: Introduction, tutorial, user manual, and implementation, Technical Report 93\u201339, TU Berlin."},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"Bird, R. & de Moor, O. (1997), Algebra of Programming,Prentice Hall International.","DOI":"10.1007\/978-3-642-61455-2_12"},{"key":"9_CR6","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/978-1-4612-0685-9_4","volume-title":"Beyond Calculation, Springer","author":"EW Dijkstra","year":"1997","unstructured":"Dijkstra, E. W. (1997), The tide, not the waves, in P. J. Denning & R. M. Metcalfe, eds, \u2018Beyond Calculation\u2019, Springer, pp. 59\u201364."},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Dijkstra, E. W. & Scholten, C. (1990), Predicate Calculus and Predicate Transformers,Springer-Verlag.","DOI":"10.1007\/978-1-4612-3228-5"},{"key":"9_CR8","unstructured":"Gasteren, A. J. M. v. (1987), On the Shape of Mathematical Arguments,LNCS 445, Springer-Verlag."},{"key":"9_CR9","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G. Gentzen","year":"1935","unstructured":"Gentzen, G. (1935), \u2018Untersuchungen \u00fcber das logische Schlie\u00dfen\u2019, Mathematische Zeitschrift 39, 176\u2013210,405\u2013431.","journal-title":"Mathematische Zeitschrift"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Gries, D. & Schneider, E B. (1993), A Logical Approach to Discrete Math,Springer-Verlag.","DOI":"10.1007\/978-1-4757-3837-7"},{"key":"9_CR11","unstructured":"Jones, C. B. (1990), Systematic Software Development Using VDM,second edn, Prentice Hall International."},{"issue":"2","key":"9_CR12","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1093\/comjnl\/27.2.97","volume":"27","author":"D Knuth","year":"1984","unstructured":"Knuth, D. (1984), \u2018Literate programming\u2019, The Computer Journal 27 (2), 97\u2013111.","journal-title":"The Computer Journal"},{"key":"9_CR13","unstructured":"Knuth, D. (1992), Literate Programming,Center for the Study of Language and Information."},{"issue":"7","key":"9_CR14","doi-asserted-by":"publisher","first-page":"600","DOI":"10.2307\/2974556","volume":"102","author":"L Lamport","year":"1994","unstructured":"Lamport, L. (1994), \u2018How to write a proof\u2019, American Mathematical Monthly 102 (7), 600\u2013608.","journal-title":"American Mathematical Monthly"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Paulson, L. C. (1994), Isabelle,LNCS 828, Springer-Verlag.","DOI":"10.1007\/BFb0030541"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Polya, G. (1954), Mathematics and Plausible Reasoning, Vol. 1 \u2014 Induction and Analogy in Mathematics, Vol. 2 \u2014 Patterns of Plausible Inference,Princeton University Press.","DOI":"10.1515\/9780691218304"},{"key":"9_CR17","unstructured":"Polya, G. (1957), How to Solve It,second edn, Princeton University Press."},{"key":"9_CR18","first-page":"223","volume-title":"KORSO: Methods, Languages, and Tools to Construct Correct Software","author":"T Santen","year":"1995","unstructured":"Santen, T., Kamm\u00fcller, F., J\u00e4hnichen, S. & Beyer, M. (1995), Formalization of algebraic specification in the development language Deva, in M. Broy & S. J\u00e4hnichen, eds, \u2018KORSO: Methods, Languages, and Tools to Construct Correct Software\u2019, LNCS 1009, Springer-Verlag, pp. 223\u2013238."},{"key":"9_CR19","unstructured":"Simons, M. (1997a), The Presentation of Formal Proofs,GMD-Bericht Nr. 278, Oldenbourg Verlag."},{"key":"9_CR20","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1007\/BFb0028399","volume-title":"Theorem Proving in Higher Order Logics \u2014 10th International Conference","author":"M Simons","year":"1997b","unstructured":"Simons, M. (1997b), Proof presentation for Isabelle, in E. L. Gunter & A. Felty, eds, \u2018Theorem Proving in Higher Order Logics \u2014 10th International Conference\u2019, LNCS 1275, Springer Verlag, pp. 259\u2013274."},{"key":"9_CR21","first-page":"61","volume-title":"IFIP Working Conference on Programming Concepts, Methods and Calculi (PROCOMET94), North Holland","author":"M Simons","year":"1994","unstructured":"Simons, M., Biersack, M. & Raschke, R. (1994), Literate and structured presentation of formal proofs, in E.-R. Olderog, ed., \u2018IFIP Working Conference on Programming Concepts, Methods and Calculi (PROCOMET\u201994)\u2019, North Holland, pp. 61\u201381."},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Simons, M. & Sintzoff, M. (1997), Algebraic composition and refinement of proofs, in M. Johnson, ed., \u2018Sixth International AMAST Conference (AMAST\u201997)\u2019, Springer-Verlag.","DOI":"10.1007\/BFb0000492"},{"issue":"1","key":"9_CR23","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/BF01211052","volume":"8","author":"M Simons","year":"1996","unstructured":"Simons, M. & Weber, M. (1996), \u2018An approach to literate and structured formal developments\u2019, Formal Aspects of Computing 8 (1), 86\u2013107.","journal-title":"Formal Aspects of Computing"},{"key":"9_CR24","doi-asserted-by":"crossref","unstructured":"Thurston, W. P. (1994), \u2018On proof and progress in mathematics\u2019, Bulletin (New Series) of the American Mathematical Society 30 (2).","DOI":"10.1090\/S0273-0979-1994-00502-6"},{"key":"9_CR25","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/BF01212485","volume":"5","author":"M Weber","year":"1993","unstructured":"Weber, M. (1993), \u2018Definition and basic properties of the Deva meta-calculus\u2019, Formal Aspects of Computing 5, 391\u2013431.","journal-title":"Formal Aspects of Computing"},{"key":"9_CR26","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/3-540-58555-9_109","volume-title":"FME94: Industrial Benefits of Formal Methods, LNCS 873, Springer-Verlag","author":"M Weber","year":"1994","unstructured":"Weber, M. (1994), Literate mathematical development of a revision management system, in M. Naftalin, T. Denvir & M. Bertran, eds, \u2018FME\u201994: Industrial Benefits of Formal Methods\u2019, LNCS 873, Springer-Verlag, pp. 441\u2013460."},{"key":"9_CR27","doi-asserted-by":"crossref","unstructured":"Weber, M., Simons, M. & Lafontaine, C. (1993), The Generic Development Lan-guage Deva: Presentation and Case Studies,LNCS 738, Springer-Verlag.","DOI":"10.1007\/3-540-57335-6"},{"issue":"4","key":"9_CR28","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1145\/362575.362577","volume":"14","author":"N Wirth","year":"1971","unstructured":"Wirth, N. (1971), \u2018Program development by stepwise refinement\u2019, Communications of the ACM 14 (4), 221\u2013227.","journal-title":"Communications of the ACM"}],"container-title":["Ausgezeichnete Informatikdissertationen 1996"],"original-title":[],"language":"de","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-322-91230-5_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,20]],"date-time":"2022-01-20T04:33:28Z","timestamp":1642653208000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-322-91230-5_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783519026464","9783322912305"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-322-91230-5_9","relation":{},"subject":[],"published":{"date-parts":[[1998]]}}}